Formal Verification

This is an unrefined collection of course contents related to verification (for future reference).

General

Approach
- Model checking (brute force state space; specification + constraints)
- Equivalence checking (two algorithms; compiler optimization passes)
- Symbolic methods
- Type system (disallow unsafe behavior)
Concurrency
- Sequential single process
- (Distributed) concurrent multiprocess
Decision 3
- Program verification
  - Parse native code (e.g., JavaScript) into a representation and check that representation (see LoVe and VfS below).
- Model of concept
  - (Distributed) algorithms, protocols, data structures with operations, transition systems, math concepts, hardware design.

Courses

Advanced Logic (AL)

Content

Model checking (correctness; e.g., safety and liveness properties, mutual exclusion).
- Linear Temporal Logic (LTL).
  - See: Spin.
- Computation Tree Logic (CTL; extension of PDL).
  - See: NuSMV.
- Hoare logic as subset of PDL.
Logics
- Basic Model Logic (BML).
- Basic Temporal Logic (BTL).
- Propositional Dynamic Logic (PDL; multi-modal logic).
Decidability (vs. Expressiveness: prop1, BML, pred1)
- Sequents, tableaux (potentially used in proof automation, e.g., see the LTL model checking here).
- Translation from BML to the decidable two-variable fragment of predicate logic.
- Effective finite model property (selection approach; tree unravelling).
Extra
- Security: authorization and access control policies.
- AI and Knowledge representation. Epistemic logic.

Resources

“Modal Logic for Open Minds” by Johan van Benthem.
Modal Logic Overview.

Logical Verification (LoVe)

Content

Basic definitions and theorems (properties). E.g., data structures.
- Inductive predicates for more advanced theorems, e.g., full trees, sorted lists.
Transition systems (reachability)
- Inductive predicates. With a reflexive transitive closure.
Formal semantics (specifications, languages and their programs)
- E.g., for verified interpreters, compilers, verifiers, type checkers, static analyzers (LoVe pg. 129).
1. Operational Semantics (idealized interpreter)
  - Reason about properties of a language.
  - Big-step semantics (natural semantics).
    - Reason about concrete programs, that is, relate initial states with final states.
    - Reason about properties of a language. Among others, nontermination and determinism.
  - Small-step semantics.
    - Reason about intermediate states, and thus also multithreaded programs.
    - Proof (non)termination.
2. Hoare Logic / Axiomatic Semantics (idealized verifier)
  - Program correctness/verification. Pre- and postconditions on programs.
3. Denotational Semantics (idealized compiler)
  - Reason about program equivalence and transformations (e.g., verify that compiler optimizations (or code refactoring) preserve program semantics/meaning). Focus is on compositionality; modelling semantics/meaning as a mathematical object.
Mathematical proofs
- With mathlib.
- E.g., reason about mathematical structures such as groups, fields, and linear orders.
Larger systems (LoVe, pg. viii)
- Verified hardware design
- Verified OS kernels

Resources

Using Lean 4.
VU Logical Verification 2022-2023 course (lecture videos included)
- LoVe Book 2024: Hitchhiker’s Guide to Logical Verification
- Exercise sheets 2024: repository
Theorem Proving in Lean 4
The Natural Numbers Game

Verification for Security (VfS)

Content

Hoare Logic / Axiomatic Semantics.
- Verify program correctness.
- We built a program verifier.
  - Models the language in Haskell, and has parsing from JavaScript to the Nano language. Has a VCGen built-in. Uses the Z3 solver.
  - The verification condition generator creates a set of verification conditions (formulas) automatically based on the concrete program.
  - This is like Amazon’s Dafny.
    - “Dafny is a verification-aware programming language that has native support for recording specifications and is equipped with a static program verifier.”
    - Dafny code can be compiled to Java, Python, C#, etc.
    - Tutorial.
    - Use case (post): Cedar AWS’ authorization-policy language (permissions).
      - Dafny used for verification-guided development of the model (authorization engine and validator).
      - Rust based production implementation.
      - Differential random testing (DRT; random input generation; using cargo fuzz) was used to verify that the verified Dafny model and the production implementation model the same semantics.
- SMT solver
  - Solves the formulas generated by the VCGen. Contains the DPLL algorithm, and a Linear Rational Arithmetic (LRA) theory solver (using the Simplex method).
- Automatic invariant finding through horn clauses.
- Liquid Types extends our procedural program verifier to also verify functional languages.
  - E.g., Liquid Haskell. Recommend tutorial.
Information-flow control type system
- For information security (even at the hardware level). E.g., no leaking of secrets, no side channels, speculative execution.
- Two approaches to prove non-interference
  - Verification approach (uses the techniques used for program verification described above; also called self-composition or product program; conferences: CAV)
  - Language-based security (disallow writing programs that might be wrong through a type system; programming language conferences: PLDI, POPL)

Resources

Using Haskell.
Course page.

Protocol Validation (PV)

Content

Used to verify distributed algorithms and (network) protocols. Theory from the process algebra field.
mCRL2 models the specification. μ-calculus defines constraints/properties.
We did two things:
1. State space generation:
  - Allows for model checking, that is, verifying that properties hold.
  - The downside is that a state space’s size quickly explodes when dealing with distributed algorithms.
2. Symbolic methods:
  - Allow us to reason about equivalence of two specifications.
  - Also has model checking techniques, such as Ordered Binary Decision Diagrams (then also uses μ-calculus) or Boolean Equation Systems.
There are many rewrite and optimisation techniques. E.g., to reduce the state space. Using concepts such as bisimilarity and confluence.

Resources

Using mCRL2 and μ-calculus, optionally CADP.
“Modelling Distributed Systems: Protocol Verification with µCRL (2nd edition)” by Willem Jan Fokkink.

Distributed Algorithms (Dist. Alg.) & Advanced Algorithms (AA)

Content

Reason about correctness and efficiency of algorithms through informal proofs.
The use of reductions to easily map a domain problem onto a known problem area.

Resources

“Distributed Algorithms: An Intuitive Approach” by Willem Jan Fokkink.
“Algorithm Design” by Kleinberg & Tardos.

Other

https://en.wikipedia.org/wiki/List_of_model_checking_tools