Previous Experiences

The Programatica project and Galois have each had several years of experience in the development and analysis of high-assurance systems software using functional programming, specifically the Haskell programming language.

Programatica History

Programatica developed both applications and reasoning tools for Haskell, including:

• House, a prototype operating system that boots and runs on bare metal (IA32) and in which the kernel, a small collection of device drivers, and several sample applications, have all been implemented in Haskell. The House kernel supports protected execution of arbitrary user-level binaries and manages the virtual memory of each such process by direct manipulation of the page table data structures that are used by the hardware MMU.
• Osker, a prototype separation kernel coded in Haskell. Several variants have been built, including both high-level models and simple executables.

  (For details about House and Osker, see Hallgren, Jones, Leslie and Tolmach: "A Principled Approach to Operating System Construction in Haskell".)

• A formal semantics for Haskell (including its core type system, its module system, and its dynamic semantics) that is precise enough to support mechanized formalization.
• P-Logic, a programming logic specifically designed to be faithful to Haskell's lazy evaluation semantics, and Plover, a dedicated prover for P-Logic assertions.
• Tools for embedding the GHC Core Haskell language into the HOLCF logic of the Isabelle theorem prover. This work relies on an encoding of (parts of) the formal semantics as Isabelle theory files and allows us to state and reason about the behavior of Haskell programs. (For more information, see Brian Huffman's presentations.)
• Hobbit, a prototype programming language that combines higher-order functional programming with bit-level data.

Galois History

Galois has also developed a number of Haskell applications and tools, including but not limited to:

• The Trusted Services Engine (TSE) is a highly scalable cross-domain web server and file store that lets users with differing security clearances share file-based information securely across multiple networks and domains.
• The Haskell Program Coverage (HPC) toolkit allows a programmer to identify the code exercised by a test suite.

back to main page