Entries in the “Functional Programming” 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)

Tech Talk Video: Developing Good Habits for Bare-Metal Programming

August 11th, 2010 by Iavor S. Diatchki

We are pleased to announce the availability of a new Galois tech talk video: “Developing Good Habits for Bare-Metal Programming”, presented by Mark Jones. More details about the talk are available on the announcement page.

Developing Good Habits for Bare-Metal Programming from Galois Video on Vimeo.

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

Posted in Functional Programming, Haskell, Tech Talks, Technology, Video | 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: 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)

Orc in Haskell, now on Hackage

June 14th, 2010 by john

Orc is a concurrent scripting language, now available as an embedded DSL in Haskell. I like to think of Orc as the combination of three things: many-valued concurrency, external actions (effects), and managed resources, all packaged in a high-level set of abstractions that feel more like scripting rather than programming. It provides a very flexible way to manage multiple concurrent actions, like querying remote web sites, along with timeouts and default actions.

Source code is available on Hackage; the easiest way to access it is with cabal (i.e. ‘cabal install orc’).

Also available is a draft paper entitled Concurrent Orchestration in Haskell which explains how to use Orc, as well as describing the implementation in detail.

Feedback welcome. Enjoy!

Posted in Functional Programming, Haskell | Comments (1)

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)

Tech Talk: The L4.verified Project

May 21st, 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!

IMPORTANT: Please note that this talk is Monday.

title:

The L4.verified Project

presenter:

Dr. Gerwin Klein

time:

10:30 am, 24 May 2010, Monday

location

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

abstract:

Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.

bio:

Dr Gerwin Klein is a Principal Researcher at NICTA and Conjoint Associate Professor at the University of New South Wales, Australia. He is working in the area of formal software verification, interactive theorem proving, and operating systems. He is the project leader of L4.verified. He received his PhD in 2003 from Technische Universitaet Munich on the topic of Java Bytecode Verification and has been working in the area of machine-checked formal proof in various projects since 1998.

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

Tech Talk: Developing Good Habits for Bare-Metal Programming

May 12th, 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

Developing Good Habits for Bare-Metal Programming (slides, video)

presenter

Mark Jones

High Assurance Systems Programming Project (HASP)

Portland State University

time

10:30am, Tuesday, 18 May 2010

location

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

abstract

Developers of systems software must often deal with low-level and performance-critical details that are hard to address in high-level programming languages. As a result, much of the systems software that is produced today is written in languages like C and assembly code, without the benefit of more expressive type systems or other features from modern functional programming languages that could help to increase programmer productivity or software quality. In this talk, we present an update on the status of Habit, a dialect of Haskell that we are designing, as part of the HASP project at PSU, to meet the needs of high assurance systems programming. Among other features, Habit provides: mechanisms for fine control over representation of bit-level and memory-based data structures; strong support for both functional and imperative programming; and a flexible type system that allows precise characterization of size and bound information via type level naturals, as well as termination properties resulting from the use of unpointed types.

bio

(from http://web.cecs.pdx.edu/~mpj/)
Mark Jones is a Professor in the Department of Computer Science in the Maseeh College of Engineering & Computer Science at Portland State University in Portland, Oregon, USA. His interests include all aspects of programming language design, implementation, and application. He is particularly interested in the use of advanced programming language technologies for systems programming, and in the development and application of expressive type and module systems that support the construction and certification of secure and reliable software systems.

Posted in Formal Methods, Functional Programming, Haskell, Tech Talks, Technology | Comments (2)

Solving n-Queens in Cryptol

April 11th, 2010 by Levent Erkok

The eight queens puzzle asks how to place eight queens on a chess board such that none of them attacks any other. The problem easily generalizes to n queens, using an nxn board. In this post, we’ll see how to solve the n-Queens puzzle in Cryptol, without lifting a finger!

Representing the board

It is easy to see that any solution to the n-Queens puzzle will have precisely one queen on each row and column of the board. Therefore, we can represent the solution as a sequence of n row numbers, corresponding to subsequent columns. For instance, the board pictured below (taken from the wikipedia page), can be represented by the sequence

3  7  0  2  5  1  6  4

recording the row of the queen appearing in each consecutive column, starting from the top-left position. (And yes, we always count from 0!)

Recognizing a valid solution

Let us start by asking a simpler question. How can we recognize that a given sequence of n row indices constitute a valid solution? We have to verify that the followings hold:

• The numbers must be between 0 and n-1. (Sanity checking.)
• The numbers should not be duplicated. (Ensures that there is exactly one queen per row.)
• For any pair of numbers in the sequence, their row-value difference should be different than their column-value difference. (Ensures that there are no diagonal conflicts.)

The first two conditions are fairly trivial. The last one simply says that if two queens are positioned such that their vertical and horizontal displacements are the same, then they are on the same diagonal: A situation we must avoid for all pairs of queens given.

Writing a Cryptol predicate

Having described how we will recognize an alleged solution, let us now consider how we can code this in Cryptol.

First, we will need a helper function that applies a given predicate to all the elements of a sequence and returns True if all elements satisfy the predicate. Naturally, we call this function all:

 all : {n a} (fin n) => (a -> Bit,[n]a) -> Bit;
 all (f, xs) = [|f x || x <- xs|] == ~zero;

The type of this function is worth spending a few moments looking at, as it demonstrates some crucial aspects of  Cryptol’s type system that sets it apart from other languages. In particular, it says that the function all takes a sequence of n elements, each of some arbitrary size a. However, it also restricts n to be  finite, i.e., the type system will complain if you pass all an infinite sequence. Then, we apply the predicate f to each element in the sequence, and check that the result consists of all True bits. (The polymorphic Cryptol value zero represents a value with an arbitrary shape with all bits set to False. The complement operator (~) flips all those bits to True.)

The second utility function we will need is a predicate that checks whether the elements of a given sequence are all distinct:

 distinct : {a b} (fin a,fin b) => [a]b -> Bit;
 distinct xs = diff == ~zero
   where {
     n = width xs;
     diff = [|check (x, i)
            || x <- xs
            || i <- [0 .. (n-1)]
            |];
     check (x, start) = walk (start + 1)
        where walk cur =
                if cur == n
                   then True
                   else if xs @ cur == x
                        then False
                        else walk (cur + 1);
      };

The function distinct is fairly simple: For each element in the sequence, it walk’s through the rest to make sure that none of the remaining elements are the same as that particular element. Note how Cryptol’s width function allows us to determine the size of the input sequence, and recurse properly.

Having done the heavy-lifting above, we can now write the predicate that recognizes a valid n-Queens solution in Cryptol:

type Solution(n) = [n][1+width n] -> Bit;

nQueens : {n} (fin n) => Solution(n);
nQueens qs = all(inRange, qs)
           & distinct qs
           & all(checkDiag, ijs)
  where {
     n = width qs;
     inRange x = x < n;
     ijs = [| (i, j) || i <- [0 .. n-1]
                      , j <- [0 .. n-1] |];
     checkDiag (i, j) =
        (i >= j) | (diffR != diffC)
          where { qi = qs @ i;
                  qj = qs @ j;
                  diffR = if qi >= qj
                          then qi-qj
                          else qj-qi;
                  diffC = j - i;
           };
    };

The nQueens function simply executes our checks as we described above. It first makes sure that all the elements are inRange. (Note that we do not have to check for negative numbers since all Cryptol numbers are non-negative.) Then, we check that all the elements are distinct. Following this, we generate the pairs of indices ijs, and call checkDiag on all these pairs to make sure that the row and column differences do not match.

We can test this function in Cryptol, by providing sample input:

  NQueens> nQueens [3 7 0 2 5 1 6 4]
  True
  NQueens> nQueens [3 7 0 2 5 6 1 4]
  False

In the second example, I swapped the elements 1 and 6; effectively putting the 6th queen on row 6 and the 7th on row 1. This creates a diagonal conflict  as the reader can easily verify.

Solving n-Queens

It appears that all we have done so far is to write a Cryptol program to recognize whether a given solution to the n-Queens problem is valid. But, how do we actually solve the puzzle?

Remember that I promised to solve n-Queens without lifting a finger, and this is where Cryptol’s formal methods based tools come into the picture. Given any predicate (like nQueens above), Cryptol can find inputs that will satisfy it automatically, at the push of a button! (We have briefly described how this works in our previous post on Sudoku, so I shall not go into any details. Suffice it to say that one can exploit modern SAT/SMT solvers to generate automatic solvers for validity problems, and Cryptol provides just the right framework for doing so.)

Without further ado, here is how we solve n-Queens in Cryptol, without writing any additional code on top of what we have already seen:

  NQueens> :set sbv
  NQueens> :set base=10
  NQueens> :sat nQueens : Solution(8)
  (nQueens : Solution(8))  [2 7 3 6 0 5 1 4]
  	 = True

The first command puts Cryptol in the sbv mode, which allows for the use of SAT/SMT solvers. The second command tells Cryptol to print results in base 10. Finally, the :sat command finds satisfying assignments for predicates. The type-signature on the :sat command indicates that we are interested in solutions for 8-queens, for which we are given a solution almost instantaneously!

If you look at the wiki-page for n-queens, you will see that they claim there is always a solution when n=1 and n>=4. We can indeed verify that there are no solutions when n is 2 or 3, using Cryptol:

NQueens> :sat nQueens : Solution(2)
No variable assignment satisfies this function
NQueens> :sat nQueens : Solution(3)
No variable assignment satisfies this function

While these two properties are easy to see, it’s quite valuable to get independent verification!

In practice..

We would be remiss if we didn’t mention some of the actual uses of the satisfiability checker in the Cryptol tool chain. The most important application is in verifying functional equivalence of two functions. If f and g are two functions, then they are functionally equivalent exactly when the predicate (\x -> f x != g x) is not satisfiable. (Conversely, if this predicate is satisfiable then the satisfying value is where f and g disagree, indicating a potential bug.) More importantly, f and g need not be both written in Cryptol. The toolchain allows performing equivalence checking between functions written in VHDL, C, and Java (with varying degrees of “seamless” integration!). Furthermore, this is also how we make sure our compiler produces correct code: The function g can be generated code, for instance in one of Cryptol’s intermediate languages as we compile Cryptol to FPGA descriptions. In summary, we can check the equivalence of 3rd party code (generated or hand-written) against “gold” Cryptol specifications, increasing assurance in the correctness of crypto-implementations.

Download

You can download the Cryptol solution for n-Queens. Cryptol licenses are also available free of charge at www.cryptol.net, although I should note that the SAT/SMT based backends are only available in the full-releases of Cryptol, which requires a simple form to be filled before downloading. Enjoy!

Posted in Cryptography, Formal Methods, Functional Programming, Misc, Technology | Comments (8)