Galois has been selected by AFRL/OSD for a Phase I Small Business Innovative Research (SBIR) award to develop countermeasures against malicious hardware. In this project, Galois will address the class of hardware threats known as “deterministically triggered trojans”, and develop tools that inhibit malicious hardware activation by applying attack incompatibility techniques.   This effort builds […]

Performing consistent builds is critical in software development, but the current system in GHC/Haskell of per-user and per-system GHC package databases interferes with this need for consistency. It is difficult to precisely identify the dependencies of a given project, and changes necessary to enable one project to build may render another project inoperable. If each […]

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 […]

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 […]

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 […]

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 […]

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 […]

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 […]

We are pleased to announce the availability of a new Galois tech talk video: “The Rubinius Virtual Machine”, presented by Brian Ford. More details about the talk are available on the announcement page. The Rubinius Virtual Machine from Galois Video on Vimeo. For more videos, please visit http://vimeo.com/channels/galois.

We are pleased to announce the availability of a new Galois tech talk video: “Formal Methods Applied to Control Software”, presented by Alwyn Goodloe. More details about the talk are available on the announcement page. Formal Methods Applied to Control Software from Galois Video on Vimeo. Formal Methods Applied to Control Software from Galois Video […]