Formal Methods in Use at Galois, Inc.

Sunday 10 August 2008, Sydney, Australia

A tutorial at the 4th International Joint Conference on Automated Reasoning (IJCAR 2008).

Overview

Galois, Inc. is a start-up company in Portland, Oregon that applies a combination of formal methods and functional languages to create trustworthiness in critical systems.

This half-day tutorial will use two in-depth case studies to illustrate how commercial formal methods opportunities arise, and how automated reasoning tools are applied as part of the Galois high assurance methodology.

Program

Part I: Cross Domain Solutions. The first part of the tutorial will focus on formal methods for building high assurance cross domain solutions, in which data from multiple security levels is processed in one device. Before such devices are deployed they undergo a scrutiny process to make sure that the data transferred between the different domains is specified by the security policy, or to put it another way, there is no unintended leakage. The GaloisTrusted Services Engine (TSE) cross domain solution will be used as a case study, illustrating how an assurance argument is constructed and how the Isabelle theorem prover was used to verify the critical component of the TSE.

Part II: Domain Specific Languages. The second part of the tutorial will focus on the use of domain specific languages to develop high assurance systems, using the Cryptol domain-specific language for cryptography as a case study. Work is ongoing at Galois to develop high assurance tools for compiling Cryptol programs, both to native code and to FPGAs. Ensuring that the compiler preserves the meaning of the source Cryptol program in the target code or netlist is an challenging verification problem, and different approaches have used: the minisat SAT solver; the ACL2 theorem prover; as well as the more traditional approaches of code coverage and random testing.

Target Audience

• Researchers from all areas of automated reasoning wanting to see industrial applications of formal methods.
• Students wanting to see how their skills can be commercially applied.
• People from industry wanting to see how Galois is successfully applying formal methods.

Slides

The overview slides for the tutorial are available for download: IJCAR08_talk.pdf

Contact

Joe Hurd is a Formal Methods Engineer at Galois, Inc. He completed a Ph.D. at Cambridge University on the formal verification of probabilistic programs, and his work since has included generating verified checkers from a formalized hardware property language; developing tactics using automatic proof techniques from first order logic; and creating the world’s first formally verified chess endgame database.