Announcing: Internship Available at Galois, Inc.

Galois, Inc. has a Fall 2011 internship available in Portland, Oregon, USA. PROJECT OVERVIEW: The project is a research project investigating security in the domain of embedded software in robotic vehicles. We are investigating techniques in which runtime monitoring can detect and mitigate attacks. This is a research project, and directions are open-ended. You will […]

Read More

Formally Verified Chess Endgames

On May 10 Joe Hurd gave a guest lecture at Portland State University, as part of Bart Massey‘s Computer Science course on Combinatorial Games. The topic of the guest lecture was “Formally Verified Endgame Tables”, and Joe showed how Formal Methods can be used to prove that endgame tables used by computer chess programs are […]

Read More

Galois to Help DARPA PROCEED to Change the Game

Portland, OR (April 11, 2011) – The Defense Advanced Research Projects Agency (DARPA) has awarded up to $4.7M to Galois, Inc., as research integrator for the PROCEED program (Programming Computation on Encrypted Data) whose goal is to make it feasible to execute programs on encrypted data without having to decrypt the data first.  DARPA Program […]

Read More

Galois awarded Navy/ONR project in binary instrumentation and monitoring

Galois has been selected by the Office of Naval Research for a Phase 1 Small Business Innovative Research (SBIR) award, to develop a viable real-time software execution monitoring system to protect programs against errors, regardless of the programming language the software is written in.   The approach will be based on instrumentation of binaries via […]

Read More

Galois CEO Testifies Before U.S. Congress

Galois’ CEO, Laura McKinney, was asked to testify before the U.S. Congress Subcommittee on Technology and Innovation on the role of small business in innovation and job creation. The hearing was specifically assessing the Small Business Innovation Research (SBIR) and Small Technology Transfer Research (STTR) programs. Laura provided background on Galois as a small business […]

Read More

Instilling Morality in Machines

Our own David Burke gave a talk on Wednesday at Portland State University as a speaker in the ‘Nuts and Bold Ideas‘ seminar series.  David described work done on multiagent simulations of morality during strategic interactions.  He explained how various agents in the simulations make choices about whether to cooperate based on each agent’s weighting […]

Read More

Merging SMT solvers and programming languages

Galois is in the business of building trustworthy software. Such software will have well-defined behavior, and that behavior is assured in some way, whether via model checking, testing, or formal verification. SMT solvers — extensions to SAT solvers with support for variables of non-boolean type — offer powerful automation for solving a variety of assurance […]

Read More

Quick authentication using mobile devices and QR Codes

Isaac Potoczny-Jones February 18, 2014: This project has recently been spun-out into a new startup company, Tozny – read more about this world-class, secure login technology at www.tozny.com. Introduction In this blog post, we propose an authentication scheme using QR codes and Internet-connected smart phones to allow a user to quickly sign into a web site without having […]

Read More

Galois awarded AFRL/OSD project in hardware security

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

Read More

cabal-dev: sandboxed development builds for Haskell

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

Read More