Galois, Inc. Wins Two Small Business Research Awards from Federal Agencies

Galois, Inc., a Portland, Oregon research and development company, has been awarded two Phase I Small Business Innovative Research contracts. Galois will be engaging with the Department of Energy and the Department of Homeland Security on innovative technology solutions.

DHS Topic: Highly Scalable Identity Management Tools

Galois has been granted a Phase I SBIR from the Department of Homeland Security to develop a reusable identity management metasystem which will be designed foundationally to support government certification for deployment across agency boundaries, focusing on open standards, secure development, and a cross-domain design.The Department of Homeland Security’s charter has a fundamental requirement to collaborate with other government agencies. Secure collaboration on this scale requires strong identity management which can “vouch for” DHS personnel working with other agencies and makes it possible to provide DHS resources to individuals in other agencies whose work requires it.Anticipated Benefits: This work will provide an opportunity to deploy standard trusted components in a variety of agencies, each of which can continue to maintain its own method of managing identity and authorization. Agencies can share information based on this layer, which will evolve to support a wide variety of needs.Potential commercial applications: Compliance with government standards of trustworthiness in software used for critical purposes, along with a user-centric approach to identity management, can enable Internet users to merge their many usernames and passwords, allow critical transactions to be executed with a higher degree of trust, and help bring about an environment where e-voting increases voters’ trust in the validity of the outcome of elections.

DOE Topic: Grid 2.0: Collaboration and Sharing on the Grid

Galois has been granted a Phase I SBIR from the Department of Energy to implement a Web 2.0 collaboration system based on Grid technologies. Galois’ system will allow dispersed scientific teams to collaborate effectively on large amounts of data produced by collections of networked computers.Grid computing makes accessible significant computational and data resources to distributed teams of scientific researchers. In doing so, it also poses a challenge: How do distributed teams collaborate effectively with these resources?The problem is determining how best to apply social and collaboration software techniques to improve the efficiency of collaboration between distributed teams working on grid systems.Potential Commercial Applications: Grid computing is inherently social in the sense of involving multiple, loosely connected parties. Social collaboration in the area of large datasets is relevant to industrial and academic scientists.

About Galois, Inc.

Galois is a research and development company with a strong drive to transition technology from research into practice in the commercial and government sphere. Located in downtown Portland, Galois is a company of around 35 employees, including software developers, project managers, and business development personnel. Galois has experience in programming language design and compiler implementation, secure web application development, secure operating system development, and several other fields. Since its founding in 1999, Galois has been funded for R&D by members of the Intelligence Community and the DoD.  Read more about Galois’ research and technology on their web site:

Read More

Achronix and Signali: High-performance 128-bit AES cores for Speedster FGPAs

Achronix Semiconductor, maker of the world’s fastest FPGAs, today announced (.pdf) the availability of new, high-performance AES IP cores for its SpeedsterTM 1.5 GHz family FPGAs.These high-performance 128-bit key size AES core are targeted at 10 Gbps, 40 Gbps, and 100 Gbps applications have been designed and built by Signali, a Galois spinoff focusing on custom cores targetting computationally intensive algorithms, fixed-function DSP and cryptographic applications. Signali uses their Quattro™ compiler suite to transform high-level descriptions of data-intensive functions, such as AES into high-performance RTL.Read the full story.

Read More

FMCAD and AFM Submissions Open

I am on the program committees for two upcoming formal methods conferences: Formal Methods in Computer-Aided Design (FMCAD), the preeminent conference on formal methods in hardware and systems, and Automated Formal Methods (AFM), a workshop on the application, usage, and extension of formal methods tools, particularly focusing on SRI’s tool suite (including a theorem prover, model-checkers, and SMT solver).Please consider submitting papers!  The deadline for FMCAD is May 22 (with abstracts due May 15); the deadline for AFM is April 30.  FMCAD will occur in Austin, Texas November 15-18, and AFM will be colocated with CAV in Grenoble, France.

Read More

One Million Haskell Downloads…

Galois engineers write a lot of Haskell (in fact, our technology catalogue is built pretty much entirely on it). We find we’re able to build systems faster, with fewer errors, and in turn are able to apply techniques to increase assurance, helping us deliver value to our clients. We’ve successfully engineered large systems in the language for nearly a decade. We also use and write a lot of open source Haskell code. Since 2004 we’ve been investing in improving packaging and distribution infrastructure for Haskell code, and since 2007 Galois has been hosting the central online database of open source Haskell libraries and applications. These packages are built via Cabal (dreamed up by Galois’ own Isaac Potoczny-Jones), and distributed via cabal-install. Hackage now hosts more than 1100 released libraries and tools, and has been growing rapidly (and, incidentally, Galois employees have released or been significant contributors to just shy of 10% of all Hackage projects).We’ve wondered for a while now just how busy Hackage was becoming, and in turn, what other interesting information about Haskell were buried in the Hackage logs. This post answers those questions for the first time. We’ll see

  • Total, and growing, Haskell source downloads
  • The most popular Haskell projects hosted on Hackage
  • The most popular development categories
  • The most popular methods for distributing Haskell source

and speculate a little on where Hackage is heading.


We’ve known for a while that uploads to Hackage were growing. You might have seen this graph elsewhere (it’s derivable from the RSS logs of package uploads):

There’s a pretty clear trend upwards. Average daily Hackage releases have increased 4-fold since Hackage was launched, and it’s now averaging 10 packages a day released. The question is: was anyone using this code?

Read More

Call for Proposals: CUFP 2009

Commercial Users of Functional Programming Workshop 2009:Functional Programming as a Means, Not an EndSponsored by SIGPLANCo-located with ICFP 2009Edinburgh, Scotland, 4 September 2009Galois is excited to promote this sixth annual event and encourages any interested in speaking at the workshop to send in a presentation proposal!  Whether you’d like to offer a talk yourself or you’d have someone in mind you’d like to nominate, please submit a proposal by 15 May 2009 via e-mail to francesco(at)erlang-consulting(dot)com or jim(dot)d(dot)grundy(at)intel(dot)com. Include a short description (approx. one page) of what you’d like to talk about or what you think your nominee should give a talk about.Do I have a presentation idea?If you use functional programming as a means rather than as an end (or could nominate someone who does), we invite you to offer to give a talk at the workshop. Talks are typically 25 minutes long but can be shorter and aim to inform participants about how functional programming plays out in real-world applications. Your talk does not need to be highly technical, and you do not need to submit a paper!What is the goal?The goal of the CUFP workshop is to act as a voice for users of functional programming and to support the increasing viability of functional programming in the commercial, governmental, and open-source space. The workshop is also designed to enable the formation and reinforcement of relationships that further the commercial use of functional programming.Tell me more!CUFP 2009 will last a full day and feature a keynote presentation from Bryan O’Sullivan, co-author of Real World Haskell. The program will also include a mix of presentations and discussion sessions varying over a wide range of topics.This will be the sixth CUFP;  for more information, including reports from attendees of previous events and video of recent talks, see the workshop web site:

Read More

Galois at POPL

The Principles of Programming Languages conference, POPL 09, and its surrounding workshops is kicking off this week in Savannah, Georgia. Galwegians will be attending most of the conferences: you might be able to find Levent at VMCAI or the Twelf Tutorial, or Iavor at TLDI or POPL, and Jeff Lewis (now at Signali) will be giving a keynote at PADL. Step up and say “hello!”.

Read More

Signali: A Custom IP-Design Company

Signali Corp is the latest technology commercialization spinout from Galois, chartered with commercialization of hardware IP core design technology aimed at the FPGA and ASIC markets.  Engineers at Galois and Signali have used the proprietary technology to deliver to government prime contractors the highest performing FPGA implementations in the world for a set of common cryptographic algorithms.With this technology, Signali is well-placed to make a significant impact on the IP core market with their ability to re-tune their cores to meet the customer’s design constraints, whether speed, or power, or area. The technology is especially well suited for optimizing hardware designs of computationally complex functions such as those common in digital signal processing and cryptographic systems.Galois enlisted the experience of Brian Moore, a seasoned design engineer and lab director from Intel, to lead Signali. Moore brings over 25 years of experience in the semiconductor and energy research industries. Galois co-founder Jeff Lewis, is leading the technology development as Chief Technology Officer. Signali is currently co-located with Galois in the historic Commonwealth Building in downtown Portland, Oregon. The company is engaged with Achronix Semiconductor to develop a portfolio of very high performance IP cores for their next-generation FPGAs. Sample performance and utilization numbers for IP cores running on the Achronix Speedster FPGA can be found on the Signali website.

Read More

Cryptol, the language of cryptography, now available

Galois is pleased to announce that Cryptol, the language of cryptography, is now available to the public!Cryptol is a domain specific language for the design, implementation and verification of cryptographic algorithms, developed over the past decade by Galois for the United States National Security Agency. It has been used successfully in a number of projects, and is also in use at Rockwell Collins, Inc.

Domain-specific languages (DSLs) allow subject-matter experts to design solutions in using familiar concepts and constructs. Cryptol, as a DSL, allows domain experts in cryptography to design and implement cryptographic algorithms with a high degree of assurance in the correctness of their design, and at the same time, producing a high performance implementation of their algorithms.Cryptol allows a cryptographer to:

  • Create a reference specification and associated formal model.
  • Test the specification against published test vectors and formal assertions about state.
  • Quickly refine the specification, in Cryptol, to one or more implementations, trading off space, time, and other performance metrics.
  • Compile the implementation for multiple targets, including: C/C++, Haskell, and VHDL/Verilog.
  • Equivalence check an implementation against the reference specification, including implementations not produced by Cryptol.

The Cryptol site has further documentation and the full language specification. In this release, Galois has made a implementation of the Cryptol language available free of charge for non-commercial uses.

The trial version is available for Linux, MacOS, and Windows installations and can be downloaded at the Cryptol site. The trial version is meant for language exploration. It includes a Cryptol interpreter with QuickCheck capabilities, documentation, and examples. The open version does not compile to VHDL, C/C++, or Haskell, and does not produce the formal models used for equivalence checking.Cryptol is implemented in Haskell.

Contact Galois to obtain a full-featured version for evaluation.

Read More