[TYPES/announce] Formal Methods in Use at Galois, an IJCAR Tutorial: Call for Participation

[Joe Hurd]

Call for Participation

*************************************************************
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)

Tutorial website: http://www.galois.com/IJCAR2008.php
IJCAR 2008 website: http://www.ijcar.org/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 Galois Trusted 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.


Registration
---------------------------------------------
Register for the tutorial as part of IJCAR 2008 registration (details
are on the IJCAR website; early registration discount ends on 10
July).


Organizer
---------------------------------------------
Joe Hurd
Galois, Inc.
joe at galois.com

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.