Entries in the “Formal Methods” category

Tech Talk Video: abcBridge: Functional interfaces for AIGs and SAT solving

August 27th, 2010 by Iavor S. Diatchki

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.

Posted in Formal Methods, Functional Programming, Haskell, Tech Talks, Video | Comments (0)

Tech talk: abcBridge: Functional interfaces for AIGs and SAT solving

August 19th, 2010 by Iavor S. Diatchki

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

title:

abcBridge: Functional interfaces for AIGs and SAT solving (slides, video)

presenter:

Edward Z. Yang

time:

10:30am, Tuesday, 24 August 2010

location:

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

abstract:

SAT solvers are perhaps the most under-utilized high-tech tools that the modern software engineer has at their fingertips. An industrial strength SAT solver can solve most human generated NP-complete problems in time for lunch, and there are many, many practical problem domains which involve NP-complete problems. However, a major roadblock to using a SAT solver in your every day routine is translating your problem into SAT, and then running it on a highly optimized SAT solver, which is probably implemented in C or C++ and not your usual favorite programming language.

This talk is about the use, design and implementation of abcBridge, a set of Haskell bindings for ABC, a system for sequential synthesis and verification produced by the Berkeley Logic Synthesis and Verification Group. ABC looks at SAT solving from the following perspective: given two circuits of logic gates (ANDs and NOTs), are they equivalent? ABC is imperative C code: abcBridge provides a pure and type-safe interface for building and manipulating and-inverter graphs. We hope to release abcBridge soon as open source.

bio:

Edward Z. Yang is an undergraduate studying computer science at MIT. He has been interning at Galois over the summer and enjoying every second of it. His interests include blogging, functional programming and practical applications of computer science research. You can read his blog at http://blog.ezyang.com/

Posted in Formal Methods, Functional Programming, Haskell, Open Source, Tech Talks | Comments (0)

White Paper: High Assurance Software Development

August 12th, 2010 by Joe Hurd

Galois is pleased to announce a new white paper entitled High Assurance Software Development, written by David Burke, Joe Hurd and Aaron Tomb.

The purpose of this paper is describe how to make software assurance a part of a science of security. Software assurance as practiced is a grab-bag of techniques, heuristics, and lessons learned from earlier failures. Given the importance of software to critical infrastructures (electricity, banking, medicine), this is an untenable situation; the smooth functioning of our society depends on this software, and we need a more rigorous foundation for assessments about the trustworthiness of these systems.

In this paper we present an evidence-based approach to high assurance, in which diverse development teams can communicate in a common language to tackle the challenges of developing secure systems. Furthermore, this framework supports formal inference techniques (in particular, a trust relationship analysis), so that we can use automated reasoning to deal with scalability issues. Perhaps most importantly, an evidence-based approach lets us tailor the tools that we bring to bear on each claim: formal methods: testing; configuration management; and so forth all have their place in an assurance argument. In the end, it’s all about deploying systems where the residual risk has been minimized, given finite resources and time. Understanding this and managing it effectively is what the science of security is all about.

Posted in Formal Methods, White Papers | Comments (0)

Galois, Inc. Wins Three Department of Energy Small Business Research Awards

August 10th, 2010 by Galois

Galois, Inc., a Portland, Oregon computer science R&D company, has been awarded two 2010 Phase I SBIR research awards, and one 2010 Phase 2 award from the US Department of Energy Office of Advanced Scientific Computing Research, to conduct research into high performance computing infrastructure.

A Deployable, Robust File System for Parallel I/O

When considering high-performance parallel computers, it is easy to overlook the importance of disk storage. In this research, Galois will address the topic of disk storage for parallel computers, and create a deployable, robust file system that will reduce downtime due to faults and increase productivity through improved system performance. Galois’ will take a synthesis approach, combining several strands of existing research on the subject of file systems and transitioning it into a robust, fully-featured product. In doing so, we will utilize modern formal methods research, in the form of model checking, to validate our design and improve the reliability of our implementation. The benefits of this research will be to improve the efficiency and decrease the cost of large, parallel file systems. This work will be applicable to Department of Energy laboratories, as well as to commercial users of massive parallel or distributed storage, such as online storage and backup providers or grid storage providers.

This project builds on Galois’ experience with industrial model checking, and our prior work on file system design and implementation via formal methods.

Improved Symbol Resolution for Portable Build Systems

Modern High Performance Computing utilizes a variety of different hardware and software platforms. These differences make it difficult to develop reusable components, which leads to a significant decrease of productivity. This project will investigate the design of portable build systems that are simple, yet sufficiently robust with respect to symbol resolution, so that they are able to adapt and build software across many different platforms. This project will result in increased productivity for software developers who design portable software components. In particular, we anticipate significant benefits in the area of High Performance Computing, where the multitude of different hardware and software platforms make the problem of reusing software particularly acute.

This work takes advantage of Galois’ background in domain specific language design, and build systems, in particular, Cabal, and other system configuration software.

Collaboration and Sharing on the Grid

The goal of the “Grid 2.0″ project is to improve the ability of a distributed team of researchers to collaborate on research using grid middleware computing infrastructure. In Phase I of this project, we developed a prototype integration of a typical collaboration-oriented web application with an open source data grid middleware system, establishing that such integration is feasible. In Phase II, we directly address the weakest point for collaboration applications on grid systems: open, standardized protocols for identity management, authorization, and delegation on the grid, via a federated identity management system providing support for software authorization and delegation on the Open Science Grid. The intent is to provide a secure, open, and flexible identity management system for use on grid infrastructure projects, portable to other grid middleware systems, and interoperable with existing identity management schemes. The open source results of the research will form the basis for applications of identity management systems in commercial cloud and grid systems.

This project builds on Galois’ experience with cross-domain collaboration tools and secure identity management systems (including OpenID, OAuth, SAML and X.509) developed for several clients over the past decade.

For more information about these projects, contact Don Stewart (dons@galois.com).

Posted in Formal Methods, Functional Programming, Galois News | Comments Off

Tech talk video: PReach – A Distributed Murphi-Based Model Checker

August 9th, 2010 by Iavor S. Diatchki

We are pleased to announce the availability of a new Galois tech talk video: “PReach – A Distributed Murphi-Based Model Checker”, presented by John Erickson. More details about the talk are available on the announcement page.

PReach – A Distributed Murphi-Based Model Checker from Galois Video on Vimeo.

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

Posted in Formal Methods, Tech Talks, Technology, Video | Comments (0)

Industrial Strength Distributed Explicit Model Checking

July 27th, 2010 by Lee Pike

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

title:

Industrial Strength Distributed Explicit Model Checking

presenter:

John Erickson

time:

10:30am,  August 3rd, 2010

location:

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

Abstract:

We present PReach, an industrial strength distributed explicit state model checker based on Murphi. The goal of this project was to develop a reliable, easy to maintain, scalable model checker that was compatible with the Murphi specification language. PReach is implemented in the concurrent functional language Erlang, chosen for its parallel programming elegance. We use the original Murphi front-end to parse the model description, a layer written in Erlang to handle the communication aspects of the algorithm, and also use Murphi as a back-end for state expansion and to store the hash table. This allowed a clean and simple implementation, with the core parallel algorithms written in under 1000 lines of code. This talk describes the PReach implementation including the various features that are necessary for the large models we target. We have used PReach to model check an industrial cache coherence protocol with approximately 30 billion states. To our knowledge, this is the largest number published for a distributed explicit state model checker. PReach has been released to the public under an open source BSD license.

bio:

John Erickson is a Design Engineer at Intel Hillsboro.  He graduated with his PhD in Computer Science from The University of Texas at Austin in 2008.  Currently he is working on the validation of uncore components in a 50+ core processor using a variety of formal and dynamic techniques. Past research interests include theorem proving with a focus on lemma generation and generalization in the context of induction.

Posted in Formal Methods, Misc, Tech Talks | Comments (0)

Tech Talk: Towards a High-Assurance Runtime System: Certified Garbage Collection

June 23rd, 2010 by Lee Pike

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

title:

Towards a High-Assurance Runtime System: Certified Garbage Collection

presenter:

Andrew Tolmach

time:

10:30am, Tuesday, 29 June 2010.

location:

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

abstract:

It seems obvious that the reliability of critical software can be improved by using high-level, memory-safe languages (Haskell, ML, Java, C#, etc.). But most existing implementations of these languages rely on large, complex run-time systems coded in C. Using such an RTS leads to a large “credibility gap” at the heart of the assurance argument for the overall system. To fill this gap, we are working to build a new high-assurance run-time system (HARTS), using an approach grounded in machine-assisted verification, with an initial focus on providing certifiably correct garbage collection.This talk will describe a machine-certified framework for correct compilation and execution of programs in garbage-collected languages. Our framework extends Leroy’s Coq-certified Compcert compiler and Cminor intermediate language. We add a new intermediate language, GCminor, that supports GC’ed languages and has a proven semantics-preserving translation to assembly code. GCminor neatly encapsulates the interface between mutator and collector code, while remaining simple and flexible enough to be used with a wide variety of source languages and collector styles. Front ends targeting GCminor can be implemented using any compiler technology and any desired degree of verification, including full semantics preservation, type preservation, or informal trust. As an example application of our framework, we describe a compiler for Haskell that translates the GHC’s Core intermediate language to GCminor. (This is joint work with Andrew McCreight and Tim Chevalier.)

bio:

Andrew Tolmach has been a faculty member at Portland State University since receiving his Ph.D.in Computer Science from Princeton in 1992. His current research interests, pursued under the aegis of the PSU High Assurance Systems Programming (HASP) project, focus on high-assurance systems software development, in particular using formal verification. His past publications, mostly about functional languages, include work on operating systems in Haskell, garbage collection, compilation, debugger implementation, integration with logic languages, and lazy functional algorithms.

Posted in Formal Methods, Functional Programming, Tech Talks | Comments (0)

Tech Talk: Coverset Induction with Partiality and Subsorts: A Powerlist Case Study

June 17th, 2010 by Iavor S. Diatchki

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

title:

Coverset Induction with Partiality and Subsorts: A Powerlist Case Study

presenter:

Joe Hendrix

time:

10:30am, Tuesday, 22 June 2010.

location:

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

abstract:

Many inductive theorem provers use induction schemes derived from the recursive calls in functions definitions. This widely-used strategy is called coverset induction in the context of algebraic specifications. One challenge in applying coverset induction is that it typically requires using a total recursive function, while many operations on data structures are only meaningful on some well-formed subset of their possible inputs.

In this talk, I’ll discuss a generalization of coverset induction to handle partial constructors and operations. The generalization is implemented in the Maude ITP, and used in an extensive case study involving powerlists — a data structure introduced by J. Misra to elegantly formalize parallel algorithms based on divide and conquer strategy. Powerlists are constructed by partial operations, and it has been a challenge to naturally reason about powerlists using a formal logic that only supports total operations. We show how theorems about powerlists can be elegantly proven using the generalized coverset induction scheme implemented in the Maude ITP.

bio:

Joe is a member of the technical staff at Galois, Inc. He is interested in developing tools for making software development easier and safer. He started out developing software for civil engineers to analyze the safety of bridge foundations. He worked on automated decision procedures during his PhD at the University of Illinois. Immediately prior to joining Galois, he developed software within Microsoft’s Trustworthy Computing Initiative.

Posted in Formal Methods, Tech Talks | Comments (0)

Tech Talk Video: Databases are Categories

June 14th, 2010 by Iavor S. Diatchki

We are pleased to announce the availability of a new Galois tech talk video: “Databases are Categories”, presented by David Spivak. More details about the talk are available on the announcement page.

Databases are Categories from Galois Video on Vimeo.

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

Posted in Formal Methods, Tech Talks, Video | Comments (0)

Tech Talk: Introducing Well-Founded Recursion

June 11th, 2010 by Iavor S. Diatchki

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

titile:

Introducing Well-Founded Recursion (slides)

presenter:

Eric Mertens

time:

10:30am, Tuesday, 15 June 2010.

location:

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

abstract:

Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of well-founded recursion as a tool for implementing recursive functions. It implements these concepts in the Agda programming language and demonstrates the technique by implementing a simple version of Quicksort.

bio:

Eric is a member of the technical staff at Galois, Inc., where he holds roles in software design and development for projects focusing on secure collaboration and secure network protocols. He specializes in Haskell programming and in leveraging Haskell’s unique type-system to improve various network and web-focused interfaces.

Posted in Formal Methods, Functional Programming, Tech Talks | Comments (1)