Tech Talk: Type-directed compilation in the wild: Haskell and Core

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note the unusual day for this talk; it is on Monday.

title: Type-directed compilation in the wild: Haskell and Core
speaker: Simon Peyton Jones
time: Monday, 29 July 2013, 10:30am
location: Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: Academic papers often describe typed calculi, but it is rare to find one in a production compiler. Indeed, I think the Glasgow Haskell Compiler (GHC) may be the only production compiler in the world that really has a remorselessly statically-typed intermediate language, informally called "Core", or (when writing academic papers) the more respectable-sounding "System FC".

As real compilers go, GHC's Core language is tiny: it is a slight extension of System F, with letrec, data types, and case expressions. Yet all of Haskell (now a bit of a monster) gets translated into it. In the last few years we have added one new feature to Core, namely typed (but erasable) coercions that witness type equalities, which turn Core into a particular kind of proof-carrying code. This single addition has opened the door to a range of source-language extensions, such as GADTs and type families.

In this talk I'll describe Core, and how it has affected GHC's development over the last two decades, concentrating particularly on recent developments, coercions, evidence, and type families.

To test your mettle I hope to end up with the problem we are currently wrestling with: proving consistency of a non-terminating rewrite system with non-left-linear rules.

bio: Simon Peyton Jones, MA, MBCS, CEng, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research (Cambridge) in 1998.

His main research interest is in functional programming languages, their implementation, and their application. He has led a succession of research projects focused around the design and implementation of production-quality functional-language systems for both uniprocessors and parallel machines. He was a key contributor to the design of the now-standard functional language Haskell, and is the lead designer of the widely-used Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages.

More generally, he is interested in language design, rich type systems, software component architectures, compiler technology, code generation, runtime systems, virtual machines, and garbage collection. He is particularly motivated by direct use of principled theory to practical language design and implementation -- that's one reason he loves functional programming so much. His home page is at http://research.microsoft.com/~simonpj.


Tech Talk: SMACCMPilot: flying quadcopters using new techniques for embedded programming

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title:SMACCMPilot: flying quadcopters using new techniques for embedded programming

speaker:Pat Hickey
time:Tuesday, 02 July 2013, 10:30am
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: At Galois, we're building critical flight control software using new software methods for embedded systems programming. We will show how we used new domain-specific languages which permit low-level hardware manipulation while still providing guarantees of type and memory safety. The flagship application for these new languages is called SMACCMPilot, a clean slate design of quadcopter flight control software built on open-source hardware. This talk will introduce our new software methods and show how we built SMACCMPilot to be high assurance without sacrificing programmer productivity.

bio: Since 2011, Pat Hickey has been a Member of Technical Staff at Galois, Inc. He has worked as an engineer on the Autonomous Systems Hardening (ASH) project funded by the Air Force Research Lab (AFRL), and the High-Assurance Cyber Military Systems (HACMS) project funded by DARPA. Mr. Hickey has served as a core developer of the ArduPilot open source project since 2011. He has a BS in Electrical Engineering at Rutgers University.


SIMON and SPECK in Cryptol

Last week, the NSA published two families of lightweight block ciphers, SIMON and SPECK:


We've formally specified both ciphers in Cryptol:


The following sections explore some applications of our specifications.


SIMON and SPECK are cipher families: each algorithm in the family offers different security and performance based on parameters such as block size, key size, and number of rounds. In Cryptol, we can use type variables to represent these parameters. For example, consider the type signature of SIMON's encrypt function:

encrypt : {n m T j} (...) => [m][n] -> ([n], [n]) -> ([n], [n]);

Each type variable corresponds to a parameter in the cipher:

  • n is the word size (the block size is 2n)
  • m is the number of key words
  • T is the number of rounds
  • j specifies which round constant to use

The encrypt function can be instantiated with almost any values for its parameters (subject to some constraints not shown here). This gives us an elegant way to construct the variants of SIMON:

Simon32_64  = encrypt `{n=16, m=4, T=32, j=0};
Simon48_72  = encrypt `{n=24, m=3, T=36, j=0};
Simon48_96  = encrypt `{n=24, m=4, T=36, j=1};
Simon64_96  = encrypt `{n=32, m=3, T=42, j=2};
Simon64_128 = encrypt `{n=32, m=4, T=44, j=3};

We can also experiment with stronger or weaker variants of the cipher:

simon> :let weakSimon = encrypt `{n=8, m=4, T=16, j=0}
simon> :type weakSimon
weakSimon : [4][8] -> ([8],[8]) -> ([8],[8])


An important property of block ciphers is that decryption is the inverse operation of encryption. We can state this property in Cryptol for the Speck64_96 encryption function (and its corresponding Speck64_96' decryption function) as follows:

theorem correctSpeck64_96: {k b}. Speck64_96' k (Speck64_96 k b) == b;

The theorem is universally quantified over all keys k and all blocks b.

We can use Cryptol's :check command to test whether the theorem holds for several randomly generated inputs:

speck> :check correctSpeck64_96
Checking case 1000 of 1000 (100.00%) 
1000 tests passed OK
[Coverage: 0.00%. (1000/1461501637330902918203684832716283019655932542976)]

However this did not give us good coverage of the state space. Instead, we can use Cryptol's :prove command to show the theorem holds for every possible input:

speck> :prove correctSpeck64_96

Cryptol proves the theorem by asking a SAT solver whether the negation of the theorem is satisfiable. If the negation is satisfiable, Cryptol returns the satisfying assignment as a counterexample to the theorem. In this case, the SAT solver says the negation is unsatisfiable so the theorem holds. The proof completes in less than 30 seconds!


Tech Talk: The Constrained-Monad Problem

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title:The Constrained-Monad Problem

speaker: Neil Sculthorpe
time: Tuesday, 25 June 2013, 10:30am
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: In Haskell, there are many data types that would form monads were it not for the presence of type-class constraints on the operations on that data type. This is a frustrating problem in practice, because there is a considerable amount of support and infrastructure for monads that these data types cannot use. This talk will demonstrate that a monadic computation can be restructured into a normal form such that the standard monad class can be used. The technique is not specific to monads --- it can also be applied to other structures, such as applicative functors. One significant use case for this technique is Domain Specific Languages, where it is often desirable to compile a deep embedding of a computation to some other language, which requires restricting the types that can appear in that computation.

bio: Originally from England, I did my PhD in the Functional Programming Laboratory at the University of Nottingham, on the topic of Functional Reactive Programming. I moved to the University of Kansas last year, where I'm a post-doc in the Functional Programming Group. Most of my time is spent working on the HERMIT project, a toolkit for the interactive transformation of the Glasgow Haskell Compiler's core language. I'm principally a Haskell programmer, and my research interests include type systems, equational reasoning, domain-specific languages and program transformation. Webpage: http://www.ittc.ku.edu/~neil/


Tech Talk: Non-interference and Binary Correctness of seL4

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

Please note that this talk is on Friday, at 11am

title:Non-interference and Binary Correctness of seL4

speaker:Gerwin Klein and Thomas Sewell, NICTA
time: Friday, 14 June 2013, 11:00am
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code.

The first part of the talk presents a new non-interference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain.

The binary proof addresses the compiler-correctness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assembly-like programs powered by modern SMT solvers. We cover the previously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1.

bio: Thomas Sewell has worked in the verification group at NICTA for seven years as a staff engineer and Isabelle/HOL proof specialist. Thomas was part of the seL4 proof effort from the beginning, working on the functional correctness proof and later proofs of security properties. He has recently begun joint work with Magnus Myreen (Cambridge University) to work on binary verification for the compiled kernel, and has also recently enrolled at UNSW as a PhD student on this project.

Gerwin Klein is Principal Researcher at NICTA, Australia's National Centre of Excellence for ICT Research, and Conjoint Associate Professor at the University of New South Wales in Sydney, Australia. He is leading NICTA's Formal Methods research discipline and was the leader of the L4.verified project that created the first formal, machine-checked proof of functional correctness of a general-purpose microkernel implementation in 2009. He joined NICTA in 2003 after receiving his PhD from Technische Universität München,Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL.

Gerwin has won a number of awards together with his team, among them the 2011 MIT TR-10 award for the top ten emerging technologies world-wide, and NICTA's Richard E. Newton impact award for the kernel verification work.

Page 1 ... 3 4 5 6 7 ... 49 Next 5 Entries »