Copilot and the Arduino

Copilot is an embedded domain-specific language designed by Galois, that allows you to generate assured, embedded C code from programs written essentially as Haskell lists (using Atom as a backend for the C code generation).  Lee Pike has written a tutorial on how to use Copilot to program an Arduino controller to play “Jingle Bells”. Read the full tutorial on […]

Read More

Galois chosen for DARPA project in Android security

DARPA has selected Galois, Inc for a Phase 1 project to develop software tools to enforce inter-application security on the Android operating system. The goal of the project is to prevent untrusted applications from accessing sensitive data or capabilities (such as GPS), whether directly, or through intermediary applications on a device. The proposed tools will address […]

Read More

Building a business with Haskell: Case Studies: Cryptol, HaLVM and Copilot

During BelHac, the Ghent Haskell Hackathon in November, we took an afternoon session for a “Functional Programming in Industry” impromptu workshop. The following are slides I presented on Galois’ experience building a business using our functional programming expertise, in particular, Haskell. The talk describes three case studies where “functional thinking” helped shape the solution to […]

Read More

Galois, Inc. Wins Two United States Army Research Awards

Galois, Inc. has been awarded two 2010 Small Business Innovation Research Awards by the United States Army Research, Development and Engineering Command, to investigate new approaches in the construction of high assurance microkernels, and, separately, tools for portable, consistent user interfaces based on domain specific languages. This work will be conducted under Galois’ Systems Software and […]

Read More

Galois wins NASA award for formal methods in machine learning

NASA has awarded Galois, Inc. a Small Business Innovation Research award to conduct research into the application of formal verification to machine learning systems. From the abstract: Automated tools are quickly making inroads into casual computing environments, solving progressively more complex tasks. However, these advancements still require trading reliability for convenience. Frequent minor failures are […]

Read More

John Launchbury named ACM Fellow

Chief Scientist and founder of Galois, Inc, John Launchbury, has been named a 2010 ACM Fellow by the Association for Computing Machinery (ACM). The awardees,   … ACM Fellows, from the world’s leading universities, corporations, and research labs, achieved accomplishments that are driving the innovations necessary to sustain competitiveness in the digital age … [and] celebrates […]

Read More

Galois releases the Haskell Lightweight Virtual Machine (HaLVM)

Galois, Inc. is pleased to announce the immediate release of the Haskell Lightweight Virtual Machine (or HaLVM), version 1.0. The HaLVM is a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal.” Internally, Galois has used this system in several projects with much success, and we […]

Read More

Cryptol Course: High-assurance Cryptographic Development Using the Cryptol Workbench

Galois is offering a four‐day Cryptol course for those interested in exploring the capabilities of the Cryptol workbench.The course is highly participatory: we will work on a series of exercises for each new topic, using the Cryptol toolset interactively. Prospective participants should have experience writing programs and some knowledge of cryptography. Those who complete the course will have the skills necessary to develop high‐assurance, high‐performance cryptographic algorithms in Cryptol. A tentative outline and further information can be found in the course flyer. Interested parties should contact Dr. Sally Browning via e-mail at sally@galois.com, or call her at (503) 808 7151.

Read More

Monitoring Distributed Real-Time Systems: A Survey and Future Directions

Monitoring Distributed Real-Time Systems: A Survey and Future DirectionsAlwyn Goodloe (NIA) and Lee Pike (Galois, Inc), NASA Langley Research Center, 2010.

Runtime monitors have been proposed as a means to increase the reliability of safety-critical systems. In particular, we explore runtime monitors for distributed hard real-time systems, such as fault-tolerant data buses and control systems for avionics and spacecraft. This class of systems has had little attention from the monitoring community. We motivate the need for monitors by discussing examples of avionic systems failure. We then describe work in the field of runtime monitoring. We present potential monitoring architectures for distributed real-time systems, and then we discuss how those architectures might be used to monitor properties of real-time distributed systems.

Read More