Monday
Sep232013

Galois Awarded DHS Project: Roots of Trust for Mobile Devices

Galois is delighted to announce that our proposal "Practical Roots of Trust for Mobile Devices" has been selected for award by the Department of Homeland Security. In this Phase I Small Business Innovative Research (SBIR) award, Galois will be investigating methods to provide secure yet practical methods for mobile devices to authenticate to critical systems. This work builds on Galois' expanding experience in mobile device security, including our previous work with SRI and United States Marine Corps.

Contact Leah Daniels at 503-808-7152 for more information.

Monday
Sep232013

Galois Awarded Phase II SBIR with Office of Naval Research: Programmer Intention Capture Tool (PICT)

Galois has been selected by the Office of Naval Research (ONR) for a Phase II Small Business Innovative Research (SBIR) award, for its PICT tool that interactively captures and manages programmers' intentions.

The design of a software product often isn't fully captured by the semantics and syntax of the language - many aspects of the design reside in documents, in the heads of programmers, and other places not easily analyzed. PICT is a mechanism to capture these programmer "intentions" in such a way that static analysis tools can be guided to check how the code and these intentions match up. By providing a mechanism for essentially scripting static analysis methods, we reduce the difficulty of taking advantage of them to analyze code for a wide variety of intentions.

Contact Leah Daniels at 503-808-7152 for more information.

Thursday
Sep122013

Tech Talk: Chris Anderson on Using Drones in Agriculture

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

This talk is on Friday at 2pm.

title: Using Drones in Agriculture
speaker: Chris Anderson
time: Friday, 20 September 2013, 2pm
location: Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: Small unmanned aircraft---more often called drones---are set to make a big impact on agriculture. You already know about military drones operating overseas, and perhaps you've even seen recreational drones starring in youtube videos, but as the FAA begins permitting commercial use of unmanned aircraft in 2015, you'll see drones replacing all sorts of roles that used to require a manned aircraft, and taking on new roles made possible by their low cost, versatility, and safety.

Chris Anderson will speak about the upcoming role of drones in agriculture, a field Chris says "is a big data problem without the big data." Chris will describe how farmers can will drones to curb plant disease, conserve water, and reduce pesticide and fertilizer use. He'll discuss the challenges ahead to integrate air vehicle systems with sensors, specialized cameras, and data processing.

bio: Chris Anderson is the CEO of 3D Robotics, a manufacturer of drone autopilots and complete drone systems based on open source hardware and software. He is also the founder of DIYDrones.com, the bestselling author of "Makers", and the former Editor in Chief of Wired Magazine.

Wednesday
Sep112013

High-Assurance Base64

Author: David Lazar

Galois' mission is improving the trustworthiness of critical systems. Trustworthiness is an inherent property of a system, but we need to produce evidence of its trustworthiness in order for people to make informed decisions. The evidence, and its presentation is a key part of what is often called an assurance case.

The kinds of evidence that make up an assurance case can differ, depending on how critical the system is. The more critical, the more thorough and convincing the assurance case should be. Formal methods — mathematical proofs of software correctness — are often called for when evaluating the most critical systems. A formal method approach to assurance produces a strong argument about a model of the system. In contrast, testing produces a weak argument about the system itself. The reason it is a weak argument is that for any non-trivial component, testing will only exercise a minuscule percent of the possible input space. In contrast, a formal proof says that for a model of the system, some property holds for all inputs. Phrased this way, it's clear that testing and formal evidence provide complementary evidence of a system's correctness.

In this post we describe a fast, formally verified C implementation of Base64 encoding. The 10,000 foot description of the proof approach is:

  • choose the system,
  • create a formal specification of the system,
  • create a model of the implementation, and
  • prove that the implementation meets the specification.

The code and proof are available here:

https://github.com/davidlazar/base64

The following sections describe the different parts of this repository.

The C Code

The C code in base64encode.c is a fast implementation of Base64 encoding. It is based on libb64, which uses coroutines to achieve speed. The nontrivial control-flow of this code makes proving it correct more challenging. This is the artifact we want to develop assurance evidence for.

Typing "make" at the top of our repository builds the b64enc tool, a simple frontend to the C code. Here is a quick timing comparison between our code and the base64 utility that is part of GNU Coreutils:

$ time b64enc 500MB.random > x.b64
real: 1.197s  user: 0.61s  cpu: 0.48s

$ time base64 -w0 500MB.random > y.b64 real: 2.615s  user: 1.81s  cpu: 0.62s

$ diff -w x.b64 y.b64 $

The Cryptol Specification

The Cryptol specification in base64.cry is based on RFC 4648. Ignoring padding and assuming Cryptol is in big-endian mode, the encoding routine is just two lines:

encode : {a c} (fin a, c == (8 * a + 5) / 6, 6 * c >= 8 * a) =>
        [a][8] -> [c][8];
encode xs = [| alphabet @ x || x <- groupBy(6, join xs # zero) |];

The corresponding decode function is similarly short. The b64encode and b64decode functions are wrappers around encode and decode that handle padding.

Our specification provides the following correctness theorem, polymorphic over all lengths of x:

theorem b64encodeLeftInv: {x}. b64decode (b64encode x) == x;

Cryptol can't prove polymorphic theorems on its own, so we must monomorphize the theorem to prove it:

base64> :prove (b64encodeLeftInv : [16][8] -> Bit)
Q.E.D.

base64> :prove (b64encodeLeftInv : [200][8] -> Bit) Q.E.D.

The Proof

This proof/ subdirectory contains infrastructure for proving the C code correct. The Makefile in this directory orchestrates the proof. Typing make n=16 generates and proves a theorem that says the base64_encode function from the C code (as compiled by Clang) is equivalent to the b64encode function in the Cryptol specification for the given input length n:

$ make n=16
Proving function equivalent to reference:
encode_aig : [16][8] -> [24][8]
Q.E.D.

Let's see what the Makefile is doing behind the scenes.

The C code in sym_encode.c is a wrapper around our C code that passes a symbolic value to the base64_encode function. This code is compiled by Clang to LLVM bytecode.

The LLVM Symbolic Simulator (a prototype tool currently under development by Galois) is used to extract a formal model encode_aig of the LLVM bytecode. The model can be loaded into Cryptol and used like any other function:

proof> :t encode_aig
encode_aig : [16][8] -> [24][8]

proof> encode_aig "16 characters..." "MTYgY2hhcmFjdGVycy4uLg=="

In particular, we can write a theorem about this function:

theorem MatchesRef : {x}. encode_aig x == b64encode x;

...and then prove it:

proof> :prove MatchesRef
Q.E.D.

Success! Amazingly, this proof systems scales to large values of n where exhaustive checking is not feasible:

$ time make n=1000
Proving function equivalent to reference:
encode_aig : [1000][8] -> [1336][8]
Q.E.D.
real: 17.882s  user: 16.31s  cpu: 1.50s

Summary

The success of the proof gives us high confidence that our C code is correct.

To reiterate our steps:

  • choose the system — we chose Base64 encode,
  • create a formal specification of the system — we did this with a few lines of Cryptol,
  • create a model of the implementation — we used our LLVM Symbolic Simulator to generate the model from the C code, and
  • prove that the implementation meets the specification — to do this, the Cryptol tool calls out to a SAT solver to prove the AIGs are equivalent.

The weak-link of many approaches to using formal methods applied to the software correctness challenge is the model-to-code correspondence. The approach we took above addresses that weakness by automatically generating the model via symbolic simulation of a low-level representation of the program — in this case, the LLVM bytecode. This approach would miss bugs or malware in the path from LLVM to executable, but remains a compelling argument for the correctness of the C code. In critical applications, it makes sense to include the compiler in the scope of an overall assurance case.

Monday
Sep092013

(Tech Talk) New Directions in Random Testing, From Mars Rovers to JavaScript Engines

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

This talk is on Thursday.

title: New Directions in Random Testing: from Mars Rovers to JavaScript Engines
speaker: Alex Groce
time: Thursday, 12 September 2013, 10:30am
location: Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: One of the most effective ways to test complex language implementations, file systems, and other critical systems software is random test generation. This talk will cover a number of recent results that show how---despite the importance of hand-tooled random test generators for complex testing targets--- there are methods that can be easily applied in almost any setting to greatly improve the effectiveness of random testing. Surprisingly, giving up on potentially finding any bug with every test makes it possible to find more bugs over all. The practical problem of finding distinct bugs in a large set of randomly generated tests, where the frequency of some bugs may be orders of magnitude higher than other bugs, is also open to non ad-hoc methods.

bio: Alex Groce received his PhD in Computer Science from Carnegie Mellon University in 2005, and B.S. degrees in Computer Science and Multidisciplinary Studies (with a focus on English literature) from North Carolina State University in 1999. Before joining the Oregon State University faculty in 2009, he was a core member of the Laboratory for Reliable Software at NASA’s Jet Propulsion Laboratory, and taught classes on Software Testing at the California Institute of Technology. His activities at JPL included a role as lead developer and designer for test automation for the Mars Science Laboratory Curiosity mission's internal flight software test team, and lead roles in testing file systems for space missions. His research interests are in software engineering, particularly testing, model checking, code analysis, debugging, and error explanation and fault localization.

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