1. 9
  1.  

  2. 4

    This is an amazing piece of engineering work. The language integrated ability to discharge proofs of the integrity of cryptographic protocols to SMT solvers is way ahead of its time.

    1. 3

      Here’s an example of how such a tool is integrated in an overall flow for high-assurance security:

      http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf

      I chose this one since it takes it down to CPU microcode using AAMP7G: a CPU verified mathematically to be correct and enforce separation a la seL4. The other end at Rockwell is model-driven development with Simulink or Stateflow converted to provers for correctness, then SPARK Ada for correctness, and then AAMP7G for correct execution. Correctness is from requirements in human-inspected model down to microcode.