Advanced Topics in Formal Methods

Course details

• 10 weeks, Tue/Thu, 10:30-11:50

• https://​web.​stanford.​edu/​class/​cs357/​

• Weekly readings

• 3 Assignments and a project

• Credit or letter of recommendation.

Whiparound

Introduce yourselves:

• Name

• Level of studies

• Interest/experience with formal methods

• Mnemonic - give us a fun fact about yourself

Motivation

• Patriot Missile Failure

• Pentium I FDIV bug

• Ariane 5

• The Millenium Bug

• Java's Tim Sorting bug

Formal Methods

What are Formal Methods?

So you want to use formal methods?

Mathematical model of the system:

• Computer easy
• Airplane complicated

Specification of the problem/property:

• Formal Language - Boolean logic, FOL, LTL/CTL, etc.
• Automatic vs. Manual vs. Impossible

Method to proove the property

• Proof calculus, decision procedures Enter Automated Reasoning

What is Automated Reasoning

What is reasoning?

Deductive vs. Inductive vs. Abductive

Formal proof system:

• Axioms
  • Reflexivity:
  • Symmetry:
  • Transitivity:
• Inference rules:

Search for a proof!

What is a proof?

Proof - Sequence of steps from assumptions to conclusion convincing to a sceptic

What is the correct step size?

Small vs. Big vs. Gap

Computers can only perform small steps.

What is actually hard in a proof?

What kind of systems are we looking at?

Finite and Infinite state systems:

• Unbounded data structures:
  • stacks, queues, counters, clocks, etc.
• Unbounded control structures:
  • parametrized systems, multi-threaded, concurrent programs, …

Properties:

• Safety - system does not fail catastrophically

• Security - system is free from vulnerabilities

• Verification - system behaves as intended

Formal Methods Tools

SATisfiability solvers

• MiniSAT, Lingeling, Glucose, CryptoMiniSAT,…

Satisfiability Modulo Theory solvers

• Z3, CVC4, Yices, MathSAT, Boolector,…

Automated Theorem Provers

• Vampire, E, Satallax, iProver, …

Interactive Automated Theorem Provers

• Isabelle, Coq, Lean, Agda, …

Model Checkers

• SPIN, UPPAAL, PRISM, NuSMV, CBMC, CoSA …

Satisfiability

Answering yes/no questions …

SATisfiability

Satisfiability Modulo Theories

Propositional Satisfiability

• First NP-complete problem Cook/Levin theorem 1971

  • Reducible to a landscape of other NP-complete problems
  • text-book example of intractable

• DP/DPLL procedure in 1960s, CDCL in early 2000s

  • Handles formulas with millions of variables and clauses.

• Swiss Army Knife of combinatorial problem solving:

  • Scheduling, Packing, Coloring, Pathing, etc.

Performance of SAT solvers

A map of SAT solving

Classes of problems

Success stories and Challenges

Four Color Theorem

Pythagorean Triples Problem

Consider all partitions of {1,2,…} into finitely many parts.

Proof: Show that to be true of a finite set {1,2,…,n}:

• SAT solver: smallest such $n is 7825
• Only computational proofs exist ~ 200TB
  • Using the Cube and Conquer technique
  • Certificate is 68GB in DRAT format

B Method

• Formal method for software developement

  • Specification, Design, Proof, Code generation

• Used to synthesize code for the Paris line 14
  • 110k B loc 86k ADA loc
  • Running since 1998
  • No bugs detected to date

Zelkowa by AWS

• AWS tool for verifying policy security

• Security policy -> SMT encoding -> SMT solver

• Z3 and CVC4 for Strings/RegExps/BVs/Arithmethic

• Checks for privacy and lifetime violations of user data

Opium - Optimal Package installer

• Unlike most default package managers it is complete
• Optimizes package size or number of packages it modifies
• Uses SAT, pseudo boolean and LP solvers
• WILL NOT ATTEMPT TO REMOVE KERNEL!

Dafny

• Programming languages with verification constructs built-in
• Based on Hoare's Calculus
• Checks verification conditions at compile time
• Uses Z3 as backend engine
• https://​rise4fun.​com/​Dafny

Grasshopper based on an extension of HC called Separation Logic

Verification of Neural Networks