This is a brief description of the component tools that comprise the Ironclad toolbox.
  • Z3 is a generic SMT solver. Although SAT--boolean satisfiability--is an NP hard problem, it turns out good heuristics can solve many big problems quickly. Z3 is a big bag of such heuristics, plus "Modulo Theories" -- a layer that computes in super-boolean domains, like integer and real-valued arithmetic. We never interact directly with Z3, but its abilities (and limitations) underlie all of the verification tools we use.
  • Boogie is a verification-oriented programming language. It lets one write imperative code with modular Hoare-style contracts (requires and ensures). The Boogie tool maps Boogie programs (.bpl) into Z3 clauses.
  • Dafny is a high-level verification-oriented programming language, with features like object orientation (which we don't yet use), dynamic frames (which we should be using), and … some other reasons it's nicer than Boogie, which is why we use it. The Dafny.exe tool maps a Dafny program (.dfy) down to Boogie for verification, and can compile Dafny code to C# code, which can then be executed against the CLR.
  • Verve is a verified operating system, primarily of a garbage collector and microkernel. Its properties are specified in (trusted) Boogie. Other trusted Boogie specifies assumptions about the hardware, such as the behavior of x86 instructions. It is implemented in BoogieAsm (.basm*) and Beat (.beat*) code.
  • BoogieAsm is a subset of Boogie in which the only non-ghost (imperative) operations allowed are those specified in the trusted hardware spec. Thus, while Boogie allows x:=x+1, the same operation in BoogieAsm requires loading a register and using the add instruction. The trusted BoogieAsm tool enforces this constraint on .basm files to generate a Boogie file for verification, and also emits assembly code (stripped of the proof used by the Boogie verification) for consumption by masm, the standard macro assembler.
  • Beat is a macro assembly language over BoogieAsm. Programming in BoogieAsm involves long and ugly assembly idioms; Beat provides a cleaner, one-line abstraction to assembly instructions. The Beat tool transforms a Beat program into a BoogieAsm program which is then verified by trusted tools. No specs are written in Beat, so its transformation needn't be trusted.
  • The trusted DafnySpec tool translates a small subset of Dafny into Boogie. Trusting this tool enables us to write high-level app specs in Dafny.
  • The untrusted DafnyCC tool compiles a Dafny program into BoogieAsm modules. It works at the whole-program level to enforce that all methods have an implementation and that all implementations generate BoogieAsm verification obligations.
  • A complete Ironclad program, thus, is made from:
    • Trusted spec: Dafny application and hardware specs, transformed via DafnySpec into Boogie, plus Verve's Boogie hardware specs.
    • Untrusted implementation verified against those specs:
      • Dafny code compiled to BoogieAsm, plus
      • Verve's Beat code transformed to BoogieAsm, plus
      • Verve's raw BoogieAsm code,
all verified and emitted as an .asm file via BoogieAsm, assembled by masm, and linked into a Windows or standalone machine image.

Last edited Oct 15, 2014 at 12:19 AM by howell, version 1

Comments

No comments yet.