Verification for security
=========================

Why are we discussing this paper?
  Formal verification can eliminate bugs (prove a strong security guarantee).
  Big deal for security: many vulnerabilities are due to bugs/mistakes.
  This paper's artifact is widely used (e.g., in Firefox).
  Formal proof gives meaningful security guarantees.

What is formal verification?
  Goal: ensure there are no bugs.
  What does this even mean, and how to get there?
  From last lecture:
    Need to know when a bug occurs (or what is an incorrect execution).
    Need to consider all possible executions and check that there's no bugs.
  Both parts (definition and checking) seem tricky.

One correctness definition: compiler and/or developer puts in lots of assertions.
  This is what EXE from last lecture used as its correctness goal.
  Assertions indicate bugs, but is is enough to avoid assertions?
  Typically, want to prove some strong property about correctness or security.
  Even if program doesn't crash, want the end result to be right.
  This is typically called a specification (spec for short).
    Example: sort() produces a permutation of input in sorted order.
    Example: checkpw() returns OK if password is correct for the user logging in.
  Contrast with bug-finding: focus on overall correctness rather than the bug.
    Doesn't matter what the bug is: our goal isn't to pin-point the bug.
    No need to flag bug early like in EXE.
      We will need to reason about execution all the way to the end.
    If we prove correctness, the end result is correct for all runs.
      Doesn't matter if some code looks buggy.
      We know it's correct the way it's used to achieve the spec!

Cryptographic code has lots of subtle bugs that aren't about memory safety.
  [ Ref: https://github.com/mit-plv/fiat-crypto/blob/master/crypto-defects.md ]
  Many public-key crypto implementations operate on big numbers (>> 64 bits).
  Common technique: multiple limbs represent a bignum.
    Naive plan: 64-bit limbs, bignum is limb0 + 2^64*limb1 + 2^128*limb2 + ...
  Operations on bignums require handling carry between limbs.
    With our naive plan, every addition (or other op) propagates carry bits.
  Problem 1 with carry: control flow timing channel.
    If we just use an if statement, code will run slower when there's carry.
    Adversary could learn information about signing keys, etc.
    Better plan: compute carry bit and add it, regardless of whether it's 1 or 0.
  Problem 2 with carry: performance.
    Doing carry propagation takes time.
    Clever optimization: use a smaller limb weight than 2^64 (e.g., 2^51).
    Then, can postpone carry propagation for a while (until it gets to 2^64).
    Widely used trick in crypto library implementations.
  Similarly, bignums are usually modulo some large prime.
    Requires periodic "modular reductions".
    But again, modular reductions are expensive, want to defer when possible.
  Challenge: need to track when carry propagation / mod reduction is necessary.
    Limb values grow depending on how many ops, and which ops, are executed.
    Not doing the carry propagation / modular reduction risks incorrect result.
    Real bugs due to this problem, could lead to key disclosures, etc.

Formal verification components.
  Implementation: code the developer cares about.
  Spec: precise description of what it means for the code to be correct.
    Can think of this as an extreme version of "bug definition" from EXE.
    Actually expressed quite differently from EXE's panic/crash plan.
  Verifier: tool that checks if implementation meets spec.
    Like a sophisticated compiler / type-checker.
    Often uses an SMT solver internally, same as we saw in EXE.
    F* in the HACL* project.
  Proof: developer-written hints to the verifier to make it say "OK".
  If verifier says OK, can compile and use implementation code.

What's trusted in verification?
  Spec has to be correct / capture desired properties.
  Implementation is not trusted.
    In principle, could be supplied by an adversarial developer!
    That requires the spec to capture everything you might care about.
    Often not quite true: performance, liveness, etc.
  Verifier is trusted to be correct.
    Similar to how we trust compiler, etc.
    Could be the case that a bug in the verifier means the proof isn't right.
    Often not a big problem because implementation code isn't adversarial.
      Well-meaning developer wants to use verification to ensure correctness.
  Some verifiers have a clever design with a small trusted component.
    E.g., Coq is large but has a small proof-checking kernel.
    Only proof-checking kernel has to be correct to know a proof is valid.
    Rest of proof checker is responsible for generating proof for kernel.
    But bugs in the rest of the proof checker can't cause a bad proof to validate.
  
Verification approach: program logic.
  Hoare logic, named after Tony Hoare.
    Different way of considering possible execution paths, than what EXE did.
  Basic idea: pre- and post-conditions.
    Precondition describes what has to be true before a piece of code runs.
    Postcondition describes what will be true afterwards.
  Typically written as {P} code {Q}.
    P is the precondition.
    Q is the postcondition.
  Demo: triple from fstar/Hoare.fst
    Pre- and post-condition for triple.
    Breaking impl causes fstar to error out.
  How to verify code in Hoare logic?
    Sequence rule.
    Suppose we want to prove {P} foo; bar {Q}.
    First prove {P} foo {V}.
    Then prove {V} bar {Q}.
    E.g., F* knows the specs for <<^ and +%^ operators.
  Demo: times9 from fstar/Hoare.fst
    Can verify times9 without looking inside triple, just using its spec.

Specs ensure memory safety.
  Any spec (e.g., triple or times9 from fstar/Hoare.fst) ensures memory safety.
  If we had a memory safety violation, couldn't prove anything.
    Buffer overflow leads to undefined behavior, cannot predict outcome.
  But specification for times9 is much stronger than just "no crashes".
    Promises correct result.

Executable code: generating from F*.
  Demo so far has been writing code in F*.
    Higher-order, dependent types, etc.
  Paper's plan: translate a subset of F* code into C.
    Tool called Karamel.
    Low* is a subset of F*.
    For code in Low*, Karamel can take F* and output corresponding C.
  Demo: fstar/Hello.fst
    Spec proves memory safety, plus something about return value.
    Corrupting the code (e.g., writing past end of b) causes fstar error.
    Extracts to Hello.c, Hello.h
    Can run this from main.c

Writing more sophisticated specifications.
  Big idea: abstraction function.
    Takes code-level state and translates into an abstract version.
    Abstract state doesn't have to be efficient or executable.
    Hopefully it's helpful to describe the desired spec, though.
  Example: fsum (page 1792).
    Abstraction function eval: takes bignum limbs, returns big integer.
    Spec: function returns the sum of bignums.
    More complex at the code level, but spec is succinct.
  Abstraction functions help keep specs short.
    Also helps caller reason about what function does, in abstract terms.

Reasoning about memory.
  Need to state what's true about pointers.
  Pointers refer to a specific state of memory.
  Pre- and post-conditions refer to the heap before and after function runs.
    B.live heap ptr
    ptr is a special value ("buffer") in F* that tracks both pointer and length.
    Only the base pointer is extracted via Low* to C.
    But in F*, can reason about the buffer's logical length.
  Demo: fstar/Bignum.fst
    Simple kind of bignum, two 64-bit limbs.
    Abstraction function: eval (does not get extracted to C code).
    fadd: requires that a and b are valid pointers, in starting heap h0.
    Postcondition ensures r is a valid pointer in final heap h1,
      and abstract value of r is the sum of abstract values of a and b.
    Extra precondition to avoid overflow: a, b < 2^63.
    Generates plausible code (Bignum.c).
  Again, proof ensures memory safety, plus spec's requirements.

Side channels.
  Many possible side channels, hard to enumerate every leakage.
  Paper focuses on timing channels.
    Excludes physical channels like power analysis, RF, etc.
  Two main channels:
    Execution timing differences when operating on secret values.
    Cache contents affected by secret values.
  Common discipline: secret independence.
    Do not branch on secret values (could lead to timing differences).
    Do not divide by secret values (could lead to timing differences).
    Do not use secret values as addresses (could lead to cache diffs).
  How to do useful work when following secret-independence?
    Can compute: add, mul, copy values around, etc.
    eq_mask (page 1793): return 0x00000000 or 0xffffffff if equal or not.
    Can then mask with the result of eq_mask, constant time.
    Similar ops used to compute and propagate carry bits without branches.
  F* plan: special type for secret values.
    E.g., uint32_s.
    Works like uint32 but cannot branch, divide, use for pointer arith, etc.
  Nice example of F*'s dependent types: eq_mask spec from page 1793.
    Result type says z is a uint32_s whose value is either all-0 or all-1.

What is HACL* proving?
  Memory safety: as a side effect of F* proofs.
  Functional correctness: postconditions.
  Side channels: secret-independence enforced by types.
  No cryptographic security: different kind of proof!
    Requires reasoning about probabilities, computational limits, hardness.

How do we know the spec is right (no bugs in the spec)?
  Page 1792 top left.
  Audit.
  Execute the eval function using OCaml.
  Prove something on top of the spec.
  Prove equivalence of multiple specs.

How much effort is required?
  Table 1, page 1800.
  Substantial C code (7225 lines).
  Small specs (about 1/10x the size of the code).
  Moderate proof effort (22926 lines of proof, about 3x code size).

What's the performance?
  Table 2, page 1801.
  Comparable to / slightly faster than other C implementations.
  Slower than manual assembly implementations.
  Later work (fiat-crypto) showed it's possible to generate fast verified asm.

Summary.
  Verification is a powerful technique for ensuring correctness.
  Need a clear and correct specification.
  Big win for tricky and critical code, like crypto.
  Ongoing research on formal verification in other areas (security, reliability, etc).

===

Notes on running hacl-star on Arch Linux:

  pacman -S dotnet-runtime-6.0

  opam switch 4.14.1
  opam pin add fstar --dev-repo
  opam pin add karamel --dev-repo

  wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-debian-8.11.zip
  unzip z3-4.8.5-x64-debian-8.11.zip
  cp z3-4.8.5-x64-debian-8.11/bin/z3 ~/bin/z3-4.8.5

  git clone https://github.com/hacl-star/hacl-star
  cd hacl-star
  export HACL_HOME=$(pwd)
  ./tools/get_vale.sh
  export VALE_HOME=$(cd ../vale && pwd)
  export KRML_HOME=$HOME/.opam/4.14.1/.opam-switch/build/karamel.1.0.0
  make -j

Fstar demo notes:

  https://fstarlang.github.io/lowstar/html/Introduction.html
  cd fstar
  make
  ./demo
  cat Bignum.fst
  cat Bignum.c
  cat Bignum.h