Galois once again participated in the Bicycle Transportation Alliance’s Bike Commute Challenge, an annual September event that encourages people to bike to work.Galois finished 25th out of 256 teams in the Businesses and Non Profits with 25 – 99 Employees category. 26.4% of employee commutes to the office in September were by bike, Galois’ highest participation rate ever!

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:

Application of Computer Algebra Techniques in Verification of Galois Field Multipliers: Potential + Challenges

speaker:

Priyank Kalla

time:

10:30am, Tuesday 12 October 2010

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

Applications in Cryptography require multiplication and exponentiation operations to be performed over Galois fields GF(2^k). Therefore, there has been quite an interest in the hardware design and optimization of such multipliers. This has led to impressive advancements in this area — such as the use of composite field decomposition techniques, use of Montgomery multiplication, among others.My research group has recently begun investigations in the verification of such Galois Field multipliers. Unfortunately, the word-length (k) in such multipliers can be very large: typically, k = 256. Due to such large word-lengths, verification techniques based on decision diagrams, SAT and contemporary SMT solvers are infeasible. We are exploring the use of Computer Algebra techniques, mainly Groebner bases theory, to tackle this problem. In this talk, we will see why Groebner bases techniques look promising, while at the same time also studying the challanges that have to be overcome.

bio:

Priyank Kalla recieved the Bachelors degree in Electronics engineering from Sardar Patel University in India in 1993; and Masters and PhD from University of Massachusetts Amherst in 1998 and 2002, respectively. Since 2002, he is a faculty member in the ECE Dept. at the Univ. of Utah. His research interests are in the general areas of Logic Synthesis and Design Verification. Over the past few years, he has been investigating the use of computer algebra techniques over finite integer rings (Z/mZ) and finite fields (GF(2^m)) for optimization and verification of arithmetic datapaths. He is a recepient of the NSF CAREER award and the ACM TODAES 2009 best paper award. For more information, visit http://www.ece.utah.edu/~kalla

Dr. Lee Pike’s short abstract revisiting fault-tolerance of cyclic redundancy checks (CRCs), expanding on the work of Driscoll et al.. It introduces the concepts of Schrödinger-Hamming weight and Schördinger-Hamming distance, and argues that under a fault model in which stuck-at-one-half or slightly-out-of-spec faults dominate, current methods for computing the fault detection of CRCs may be over-optimistic.

• Paper (PDF)
• Slides (PDF)
• Haskell simulation
• Paper home

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!Please note the nonstandard day/time!

title:

Introduction to Logic Synthesis (slides, video)

speaker:

Alan Mishchenko, University of California, Berkeley

time:

10:30am, Friday 08 October 2010

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

The lecture describes the problems solved by logic synthesis. It presents functional representations and typical computations applied to Boolean networks, such as traversal, windowing, cut computation, simulation, Boolean reasoning. Presented next are And-Inverter Graphs (AIGs) that are increasingly used as a unifying representation for all problems. The lecture is finished by an overview of AIG-based solutions in synthesis, technology mapping, and formal verification.

bio:

Alan Mishchenko graduated from Moscow Institute of Physics and Technology, Moscow, Russia, in 1993, and received his Ph.D. degree from Glushkov Institute of Cybernetics, Kiev, Ukraine, in 1997. He has been a research scientist in the US since 1998.  Currently, Alan is an Associate Researcher at University of California, Berkeley.  His research interests are in developing computationally efficient methods for logic synthesis and verification.

John Launchbury presented the Orc language for concurrent scripting at the Haskell Workshop, 2010 in Baltimore.

Concurrent Orchestration in Haskell

John Launchbury

Trevor Elliott

The talk slides are available in PDF or online.

We present a concurrent scripting language embedded in Haskell, emulating the functionality of the Orc orchestration language by providing many-valued (real) non-determinism in the context of concurrent effects. We provide many examples of its use, as well as a brief description of how we use the embedded Orc DSL in practice. We describe the abstraction layers of the implementation, and use the fact that we have a layered approach to establish and demonstrate algebraic properties satisfied by the combinators.

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:

Enabling Portable Build Systems (slides)

speaker:

Rogan Creswick, Galois, Inc.

time:

10:30am, Tuesday 05 October 2010

location:

Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)

abstract:

Modern computing–and high-performance computing in particular–utilizes a variety of hardware and software platforms. These differences make it difficult to develop build systems that are robust to platform changes. Our goal is to investigate the design of portable build systems that are simple yet sufficiently robust with respect to environmental changes so that software can be easily distributed and built on, and for, myriad systems. We will discuss the current state of build tools and present options for iteratively improving the reliability and utility of existing build tools while laying the groundwork for more sophisticated and flexible build systems in the future.

bio:

Rogan Creswick joined Galois in January of 2010, bringing expertise in programming by demonstration and natural language processing. He also harbors a love for tool development that is backed by years of academic research in usability and software engineering at Oregon State University. His work in those areas improved techniques for fault location, detection, and assertion propagation in end-user programming languages.

Introducing Copilot

Can you write a list in Haskell? Then you can write embedded C code using Copilot. Here’s a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even a numbers:

fib :: Streamsfib = do"fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")"t" .= even (var "fib")where even :: Spec Word64 -> Spec Booleven w = w `mod` const 2 == const 0

Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin’s Atom Language (thanks Tom!). Copilot is specifically developed to write embedded software monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.Executing

> compile fib "fib" baseOpts

generates fib.c and fib.h (with a main() for simulation—other options change that). We can then run

> interpret fib 100 baseOpts

to check that the Copilot program does what we expect. Finally, if we have CBMC installed, we can run

> verify "fib.c"

to prove a bunch of memory safety properties of the generated program.Galois has open-sourced Copilot (BSD3 licence).  More information is available on the Copilot homepage.  Of course, it’s available from Hackage, too.

Flight of the Navigator

Copilot took its maiden flight in August 2010 in Smithfield, Virginia. NASA rents a private airfield for test flights like this, but you have to get past the intimidating sign posted upon entering the airfield. However, once you arrive, there’s a beautiful view of the James River.We were flying on a RC aircraft that NASA Langley uses to conduct a variety of Integrated Vehicle Health Management (IVHM) experiments. (It coincidentally had Galois colors!)  Our experiments for Copilot were to determine its effectiveness at detecting faults in embedded guidance, navigation, and control software.  The test-bed we flew was a partially fault-tolerant pitot tube (air pressure) sensor.  Our pitot tube sat at the edge of the wing.  Pitot tubes are used on commercial aircraft and they’re a big deal: a number of aircraft accidents and mishaps have been due, in part, to pitot tube failures.Our experiment consisted of a beautiful hardware stack, crafted by Sebastian Niller of the Technische Universität Ilmenau.  Sebastian also led the programming for the stack.  The stack consisted of four STM32 ARM Cortex M3 microprocessors.  In addition, there was an SD card for writing flight data, and power management. The stack just fit into the hull of the aircraft. Sebastian installed our stack in front of another stack used by NASA on the same flights.The microprocessors were arranged to provide Byzantine fault-tolerance on the sensor values.  One microprocessor acted as the general, receiving inputs from the pitot tube and distributing those values to the other microprocessors.  The other microprocessors would exchange their values and perform a fault-tolerant vote on them.  Granted, the fault-tolerance was for demonstration purposes only: all the microprocessors ran off the same clock, and the sensor wasn’t replicated (we’re currently working on a fully fault-tolerant system). During the flight tests, we injected (in software) faults by having intermittently incorrect sensor values distributed to various nodes.The pitot sensor system (including the fault-tolerance code) is a hard real-time system, meaning events have to happen at predefined deadlines. We wrote it in a combination of Tom Hawkin’s Atom, a Haskell DSL that generates C, and C directly.Integrated with the pitot sensor system are Copilot-generated monitors. The monitors detected

• unexpected sensor values (e.g., the delta change is too extreme),
• the correctness of the voting algorithm (we used Boyer-Moore majority voting, which returns the majority only if one exists; our monitor checked whether a majority indeed exists), and
• whether the majority votes agreed.

The monitors integrated with the sensor system without disrupting its real-time behavior.We gathered data on six flights.  In between flights, we’d get the data from the SD card.We took some time to pose with the aircraft. The Copilot team from left to right is Alwyn Goodloe, National Institute of Aerospace; Lee Pike, Galois, Inc.; Robin Morisset, École Normale Supérieure; and Sebastian Niller, Technische Universität Ilmenau. Robin and Sebastian are Visiting Scholars at the NIA for the project. Thanks for all the hard work!There were a bunch of folks involved in the flight test that day, and we got a group photo with everyone. We are very thankful that the researchers at NASA were gracious enough to give us their time and resources to fly our experiments. Thank you!Finally, here are two short videos. The first is of our aircraft’s takeoff during one of the flights. Interestingly, it has an electric engine to reduce the engine vibration’s effects on experiments.

Untitled from Galois Video on Vimeo.

The second is of AirStar, which we weren’t invo
lved in, but that also flew the same day. AirStar is a scaled-down jet (yes, jet) aircraft that was really loud and really fast. I’m posting its takeoff, since it’s just so cool. That thing was a rocket!

Untitled from Galois Video on Vimeo.

More Details

Copilot and the flight test is part of a NASA-sponsored project (NASA press-release) led by Lee Pike at Galois.  It’s a 3 year project, and we’re currently in the second year.

Even More Details

Besides the language and flight test, we’ve written a few papers:

• Lee Pike, Alwyn Goodloe, Robin Morisset, and Sebastian Niller. Copilot: A Hard Real-Time Runtime Monitor. To appear in the proceedings of the 1st Intl. Conference on Runtime Verification (RV’2010), 2010. Springer.

This paper describes the Copilot language.

• Lee Pike. Schrödinger’s CRCs (Fast Abstract). 40th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2010), 2010.

Byzantine faults are fascinating.  Here’s a 2-page paper that shows one reason why.

• Alwyn Goodloe and Lee Pike. Monitoring distributed real-time systems: a survey and future directions. NASA Contractor Report NASA/CR-2010-216724, 2010.

At the beginning of our work, we tried to survey prior results in the field and discuss the constraints of the problem.  This report is a bit lengthy (almost 50 pages), but it’s a gentle introduction to our problem space.

• Lee Pike, Geoffrey M. Brown, and Alwyn Goodloe. Roll your own test bed for embedded real-time protocols: a Haskell experience. In Haskell Symposium, 2009.

Yes, QuickCheck can be used to test low-level protocols.

• Alwyn Goodloe and Lee Pike. Toward monitoring fault-tolerant embedded systems (extended abstract). In International Workshop on Software Health Management (SHM’09), 2009.

A short paper motivating the need for runtime monitoring of critical embedded systems.

You’re Still Interested?

We’re always looking for collaborators, users, and we may need 1-2 visiting scholars interested in embedded systems & Haskell next summer.  If any of these interest you, drop Lee Pike a note (hint: if you read any of the papers or download Copilot, you can find my email).

We are pleased to announce the availability of a new Galois tech talk video: “Trust relationship modeling for software assurance”, presented by John Launchbury. This talk is an in-absentia presentation to the FAST 2010 audience.

Trust relationship modeling for software assurance from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.

When writing software that uses open source libraries, the license of a dependency is a real concern. It becomes necessary to watch for license compatibility, as well as ensure that the terms of the license are satisfied when doing a source distribution.As a first attempt at license compatibility checking, we have added some extra checks in the configure step for Cabal, so that warnings will be generated if any direct dependencies have licenses that conflict with that of the configured package [1]. However, there are some limitations to this approach. First, this doesn’t rule out the possibility that a dependency of a package that is deemed compatible will conflict with the license of your executable. Second, it doesn’t allow for a BSD3 library to depend on a GPL library, where the conflict is only produced when an executable is produced from the combination.Some licenses place requirements on how a source or binary distribution can happen. For example, the BSD3 license requires you to include its copyright notice in any distribution you make.In order to speed up this process, we decided to try to extract this information from the GHC package database. According to the GHC manual, the license file should be tracked by the package database, though upon closer inspection, that field doesn’t seem to be tracked. In order to address this shortcoming, we developed a small patch to add this functionality in GHC and Cabal [2]. Using this patched version of GHC and Cabal, we’ve developed a small tool to walk the dependencies of a cabal package, and collect the license files that they have registered in the package database.Both of these patches are available for you to try out, attached to the tickets below, though they have been accepted and are expected to make it into the next release of Cabal.[1] http://hackage.haskell.org/trac/hackage/ticket/481[2] http://hackage.haskell.org/trac/hackage/ticket/710

We are pleased to announce the availability of a new Galois tech talk video: “abcBridge: Functional interfaces for AIGs and SAT solving”, presented by Edward Z. Yang . More details about the talk are available on the announcement page.

abcBridge: Functional Interfaces for AIGs & SAT Solving from Galois Video on Vimeo.

For more videos, please visit http://vimeo.com/channels/galois.