The September 18th Galois Tech Talk will be delivered by Trent Jaeger, titled “Building Systems That Enforce Measurable Security Goals.”[Note the non-standard Friday date; instead of the usual Tuesday slot!]

• Date: Friday, September 18th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

The slides for this talk are now available.Abstract: In this talk, I will argue for an approach for building and deploying systems that enforce measurable security goals. Historically, the security community has developed “ideal” goals for security, but conventional systems are not built to satisfy such goals, leading to vulnerabilities. However, we find that building conventional systems to ideal security goals is not a practical option. Ideal security requires heavyweight tasks, such as complete formal assurance, and conventional systems depend on security enforcement in too many programs to make assurance cost-effective. As an alternative, we propose an approach where we use ideal goals as a means to gain a comprehensive understanding of which programs we depend upon for security enforcement and the risks that result from such enforcement. The result is a model that enables comprehensive evaluation of security goals and treatment of risks, once identified. In this talk, I will discuss the motivation for our approach in the development of a practical integrity model, called CW-Lite integrity. Then, I will describe two further experiments. The first examines whether user-level processes can be automatically deployed in a manner in which correct enforcement of system policy can be verified. The second examines whether virtual machine systems can be deployed in a manner in which integrity goals can be determined and verified. In these experiments, we leverage the mandatory access control enforcement of the Linux and Xen, although the talk will focus on the conceptual problems in obtaining a comprehensive view of security in conventional systems. The result of these experiments is that by making security goals measurable in conventional systems a comprehensive view of security can be obtained that enables the solution of key problems in building and deploying secure systems.Bio:Trent Jaeger received his M.S.E. and Ph.D degrees in computer science and engineering from the University of Michigan, Ann Arbor in 1993 and 1997, respectively. Trent joined the Computer Science and Engineering department at Penn State in 2005. He is co-director of the Systems and Internet Infrastructure Security (SIIS) Lab at Penn State. Prior to joining Penn State, he was a research staff member at IBM Thomas J. Watson Research Center for nine years.His research/teaching interests are in the areas of computer security, operating systems, security policies, and source code analysis for security. Trent has been active in the Linux community for several years, particularly in contributing code and tools for the Linux Security Modules (LSM) framework (in Linux 2.6) and for integrating the SELinux/LSM with IPsec (called Labeled IPsec, available in Linux 2.6.18 and above). Trent also has active interests in virtual machine systems (mostly Xen) and trusted computing hardware (Linux Integrity Measurement Architecture and its successor PRIMA).He is also active in the security research community at large, having served on the program committees of many of the major security conferences, including the IEEE Symposium on Security and Privacy, USENIX Security Symposium, ACM Conference on Computer and Communications Security, European Symposium on Research in Computer Security, Annual Computer Security Applications Conference, ISOC Network and Distributed Systems Symposium. Trent has been Program Chair of the ACM Symposium on Access Control Models and Technologies and the ACM Conference on Computer and Communications Security (Industry Track). He is the current Program Chair for the 2007 USENIX Workshop on Hot Topics in Security. He has over 60 refereed publications, and is the holder of several U.S. patents.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Substitution ciphers are one of the oldest encryption methods, dating back to at least the 15th century. In a substitution cipher, each character in the plain-text is simply “substituted” according to a predefined map. Decryption is simply the substitution in the reverse direction. Wikipedia has a nice description of these ciphers. Obviously, you wouldn’t want your bank to use such a cipher when executing your web-based transactions! But they are fun to play around, especially when entertaining kids in hot summer days. In this post, we’ll see how to code simple substitution ciphers in Cryptol, and go a step further and actually prove that our implementation is correct.

Preliminaries

The simplest form of substitution ciphers use a permutation of the input alphabet. That is, each letter in the input alphabet gets mapped to another in the same  alphabet. (Strictly speaking, input and output alphabets need not be the same, but nothing essential changes by making that assumption.) For instance, you might decide that your substitution will map ‘a’ to ‘q’, and ‘b’ to ‘d’, …, etc., making sure no two letters are mapped to the same target. Once this mapping is agreed on, all you have to do to encrypt a given message is to map each character to the corresponding element according to your predefined mapping rules.Here’s our Cryptol encoding of these ciphers. First, some preliminary declarations:

type Char = [8];type String(l) = [l]Char;type Table(n) = [n](Char, Char);

We’ll simply assume that the input consist of “characters,” each of which will be 8-bit quantities (i.e., numbers from 0 to 255). We will simply use ASCII encoding for normal English characters. This is captured by the Char type declaration above, which simply gives a convenient name for 8-bit wide words. The second type declaration captures sized-strings: For any given size l, the type String(l) represents a sequence of length l, containing 8-bit words. For instance, String(16) is the type of all sequences of length 16, containing numbers from 0 to 255 as elements. Finally a Table of size n is simply n-pairings of characters that form a substitution. Here’s the example table we will use:

cipherTable : Table(28);cipherTable = [| (x, y) || x <- plain || y <- cipher |]where { plain = "abcdefghijklmnopqrstuvwxyz .";cipher = "oebxa.cdf hijklmnzpqtuvwrygs"};

Note that our table has 28 entries (the lower-case English alphabet, plus space and the dot). A simple Cryptol sequence-comprehension succinctly zips the sequences up, forming our example table.

The August 25th Galois Tech Talk will be delivered by Adam Megacz, titled “Programming the Fleet”

• Date: Tuesday, August 25th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

[This is a continuation to the earlier tech seminar on the Fleet Architecture.]Slides for this talk are now available.Abstract: Computing has become far too complicated, as evidenced by recent high-profile chip design failures.  The Fleet project seeks to simplify processor design by replacing large irregular “cores” with simple functional units connected by a uniform switch fabric.  This simplification frees up hardware design resources, which can be reallocated to the use of ultra-high-performance circuit styles such as GasP.These benefits do not come for free: simplifying the hardware in this manner shifts complexity out of the silicon and into the compiler and programming language.  This talk will present current progress on and future plans for the challenging task of programming Fleet.Bio: Adam Megacz is a PhD candidate in Computer Science at UC Berkeley, a consultant to the VLSI Research Group at Sun Labs, and an NSF Graduate Fellow.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The July 28th Galois Tech Talk will be delivered by Joe Hurd, titled “Mathematics of Cryptography: A Guided Tour.”

• Date: Tuesday, July 28th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc., 421 SW 6th Ave. Suite 300 (3rd floor of the Commonwealth Building), Portland, OR 97204

Slides are now available.

Abstract:

In this informal talk I’ll give a guided tour of the mathematics underlying cryptography. No prior knowledge will be assumed: the goal of the talk is to demonstrate how simple mathematical concepts from algebra and number theory are used to build a wide range of cryptographic algorithms, from the familiar (encryption) to the exotic (zero knowledge proofs).

Bio:

Joe Hurd is a Formal Methods Engineer at Galois, Inc. He completed a Ph.D. at the University of Cambridge on the formal verification of probabilistic programs, and his work since has included: developing a package management system for higher order logic theories; applying automatic proof techniques for first order logic; and creating the world’s first formally verified chess endgame database.

Consider the following multiplication algorithm, coded in Mostek 6502 Assembler:

 LDX #8 ; 1; load X immediate with the 8LDA #0 ; 2; load A immediate with the 0CLC ; 3; set C to 0LOOP ROR F1 ; 4; rotate F1 right circular through CBCC ZCOEF ; 5; branch to ZCOEF if C = 0CLC ; 6; set C to 0ADC F2 ; 7; set A to A+F2+C and C to the carryZCOEF ROR A ; 8; rotate A right circular through CROR LOW ; 9; rotate LOW right circular through CDEX ;10; set X to X-1BNE LOOP ;11; branch to LOOP if Z = 0

This program comes from Wilfred Legato’s paper “A Weakest Precondition Model for Assembly Language Programs.” It multiplies the contents of the memory locations F1 and F2; each of which is 8-bits wide. The result is stored in the accumulator register A and the memory location LOW, each of which is, again, 8-bits. It holds that:

 F1 * F2 = 256 * A + LOW

when the algorithm terminates, correctly handling the overflow. It is worth spending a moment or two pondering how this algorithm works; it is not at all obvious how the multiplication is done!Legato’s challenge  (as  referred to in ACL2 circles) is to prove a deep-embedding of Legato’s algorithm correct with respect to a Mostek simulator coded in ACL2. We do not attempt to solve  Legato’s challenge in Cryptol. We are merely interested in coding and proving that Legato’s multiplier is correct in Cryptol. Our interest stems from the fact that Legato’s algorithm is a truly interesting multiplier on its own right, and we would like to make sure that a straightforward encoding of it in Cryptol can be proven correct automatically by Cryptol’s verification tools. And of course, it’s just too hard to pass up on the opportunity to  pay respect to the Mostek chip that powered the Commodore 64‘s and Atari 800XL‘s of our childhood.

A shallow embedding

The Cryptol solution to Legato’s problem will be a fairly shallow encoding of the multiplier, together with an automated proof of correctness. We choose to do a shallow encoding here since it allows us to focus on the multiplication algorithm itself, as opposed to the particulars of the underlying Mostek chip. Theorem proving based solutions (such as those given by ACL2 folks) will rightly pursue a deeper embedding of the algorithm and the Mostek architecture in general. Cryptol is not particularly suitable for deep embeddings. Representing Mostek assembly instructions directly as Cryptol functions is a much simpler and straightforward choice.Looking at Legato’s multiplier above, we will represent each instruction (from 1 to 11) as a simple state transformer, taking a simplified representation of the Mostek machine state as input and delivering a new one. We will only represent parts of the state that matter for our problem. The following Cryptol type declaration succinctly captures what we need:

 type Mostek = ( [8] // F1, [8] // F2, [8] // A, [8] // X, [8] // LOW, Bit // C (Carry), Bit // Z (Zero));

Using this state representation, each instruction in the program can be modeled as a  state transformer:

 type Instruction = Mostek -> Mostek;

This takes care of the data-flow aspect of the embedding; but the question of how to model control-flow remains. We will simply use the host-language’s control-flow features, using the quintessential functional idiom: by calling functions! This is actually easier done than said, and here’s our embedding of the first instruction of the program:

 // step1: LDX #8; load X immediate with the integer 8.step1 : Instruction;step1 (f1, f2, a, _, l, c, z) =step2 (f1, f2, a, 8, l, c, z);

Let’s spend a minute explaining this in detail. The first step in the program loads the register X with the immediate value 8. Using our state-transformer model, our step1 function will receive a Mostek state (consisting of the “current” values of F1, F2, A, X, LOW, CARRY, and ZERO). The “effect” of this instruction is to put the value 8 into the register X, leaving everything else the same. Once this is done, the control goes to the next instruction, which we model by calling the function step2 (which is yet to be defined).In this fashion, we can shallowly embed all the instructions in Legato’s multiplier, using Cryptol’s native functions and control-flow features. Of course, this is hardly a new idea, being the essence of the whole domain-specific embedded language saga: Using a rich host-language to “fake” other languages.Following the recipe set by step1, it is easy to model the next two instructions:

 // step2: LDA #0; load A immediate with the integer 0.step2 : Instruction;step2 (f1, f2, _, x, l, c, z) =step3 (f1, f2, 0, x, l, c, z);// step3: CLC; set C to 0 (Note the use of Bit False here)step3 : Instruction;step3 (f1, f2, a, x, l, _, z) =step4 (f1, f2, a, x, l, False, z);

Step 4 is equally easy in terms of control flow, but is tricky in terms of operation. After some head-scratching, one figures out that the term “rotate F1 right circular through C” means put the right-most bit of F1 in C, and put C in the first position of F1. A bizarre thing to do indeed, but that’s the beauty of Legato’s multiplier. The Cryptol translation is almost literal:

// step4: LOOP ROR F1; rotate F1 right circular through C.step4 : Instruction;step4 (f1, f2, a, x, l, c, z) =step5 (f1', f2, a, x, l, b0, z)where {[b0 b1 b2 b3 b4 b5 b6 b7] = f1;f1' = [b1 b2 b3 b4 b5 b6 b7 c];};

The use of pattern matching in getting the bits out of f1, and the construction of the new value of f1 is idiomatic Cryptol. There’s one little catch though: Apparently Mostek was a big-endian machine, having a most-significant-bit-first representation. Cryptol is little-endian. So, instead of rotating the bits to right, we  rotate them left.The fifth instruction is the first time where we use Cryptol’s control-flow to model the Mostek jump instruction:

 // step5 : BCC ZCOEF; branch to ZCOEF if C = 0.// ZCOEF is step8 in our encodingstep5 (f1, f2, a, x, l, c, z)= if c then step6 (f1, f2, a, x, l, c, z)else step8 (f1, f2, a, x, l, c, z);

In this case, we simply receive a state, and depending on the value of the carry bit (C), we either go to the next step (i.e., no jump); or go to the ZCOEF instruction, which is going to be step-8 in our model. Easy as pie!Step-6 is a replica of Step-3, clearing the carry bit:

 // step6: CLC; set C to 0step6 (f1, f2, a, x, l, _, z) =step7 (f1, f2, a, x, l, False, z);

Step-7 is the most compute intensive part of the algorithm. The Cryptol encoding is a bit complicated due to the need to determine if there was a carry in the addition. Since all Cryptol arithmetic is modular, we are forced to do the computation at an extended bit-size. Otherwise, the modeling of the ADC instruction is quite straightforward:

 // step7: ADC F2; set A to A+F2+C and C to the carry.step7 (f1, f2, a, x, l, c, z) =step8 (f1, f2, a', x, l, c', z')where {// 8-bit "modular" resulta' = a + f2 + (if c then (1:[8]) else (0:[8]));// Was there a carry? Check that "real"// result is larger than 255a'Large : [9];a'Large =(a # zero) // extend a by adding zero bits+ (f2 # zero) // same for f2+ (if c then (1:[9]) else (0:[9]));c' = a'Large > (255:[9]);// set the zero flagz' = a' == 0;};

The Cryptol idiom x # zero simply represents the value x extended on the right with 0 bits. (Remember that Cryptol is little-endian, hence the addition of zero bits on the right does not change the value.) Due to the polymorphic type of the value zero, the result has any number of bits larger than equal to the original bit-size of x. (Since we only need 9-bits i
n this case, we could have coded the same via the expression x # [False], but the former expression is more idiomatic Cryptol.)Steps 8 and 9 are similar to Step-4, using A and LOW instead of F1, respectively:

 // step8 : ZCOEF ROR A; rotate A right circular through C.step8 : Instruction;step8 (f1, f2, a, x, l, c, z) =step9 (f1, f2, a', x, l, a0, z)where {[a0 a1 a2 a3 a4 a5 a6 a7] = a;a' = [a1 a2 a3 a4 a5 a6 a7 c];};// step9 : ROR LOW; rotate LOW right circular through C.step9 : Instruction;step9 (f1, f2, a, x, l, c, z) =step10 (f1, f2, a, x, l', l0, z)where {[l0 l1 l2 l3 l4 l5 l6 l7] = l;l' = [l1 l2 l3 l4 l5 l6 l7 c];};

Step-10 simply decrements X, setting the ZERO flag appropriately:

 // step10: DEX; set X to X-1step10 : Instruction;step10 (f1, f2, a, x, l, c, z) =step11 (f1, f2, a, x', l, c, x'==0)where x' = x-1;

Finally, step-11 either jumps back to the top of the loop (step-4), or finishes the algorithm:

 // step11: BNE LOOP; branch to LOOP if Z = 0.// LOOP is step4 in our encodingstep11 : Instruction;step11 (f1, f2, a, x, l, c, z)= if zthen (f1, f2, a, x, l, c, z) // done!else step4 (f1, f2, a, x, l, c, z);

From a control-flow perspective, we indicate the end of the algorithm by simply returning the final Mostek state. It is worthwile at this point to go through the Cryptol embeddings of the instructions to see how they match-up to the Mostek assembly given by Legato.

Extracting the multiplier

Having coded Legato’s multiplier as a sequence of state transformers, we can simply call the function step1 to use it with an appropriate state. The following helper function simplifies this task for us, by loading the registers F1 and F2, and extracting the high and low bits at the end:

legato : ([8], [8], Mostek) -> ([8], [8]);legato (f1, f2, st) = (hi, lo)where {// get the relevant parts// to construct the starting state(_, _, A, X, LOW, C, Z) = st;// Run legato multiplier;// final A is hi; and final LOW is low(_, _, hi, _, lo, _, _) =step1 (f1, f2, A, X, LOW, C, Z);};

Note that legato still takes the starting machine state st as an argument. Legato’s claim (which we will shortly prove) is that the algorithm works correctly no matter what the initial state is, hence it is important to be explicit about the starting state.To see legato in action, let’s just run it on a simple input:

 legato> legato (12, 93, (9, 42, 3, 8, 1, False, True))(4, 92)

where I just made up the initial state by plugging in some random values. If Legato is right, then it must be the case that

 12 * 93 = 256 * 4 + 92

correctly computing the high and low bytes. And voila! Both sides equal 1116. Magic!

Correctness

If you do believe in magic,  you can stop reading now. But I suspect most readers of the Galois blog will be looking for something more concrete. Surely, we must be able to give a better argument than claiming witchcraft for the correctness of our implementation.Let us first formally capture what we mean by “correct,” by writing a Cryptol theorem that expresses our intuitive expectation:

theoremlegatoIsCorrect: {x y st}. x' * y' == 256 * hi' + lo'where { (hi, lo) = legato (x, y, st);hi', lo', x', y' : [16];hi' = hi # zero;lo' = lo # zero;x' = x # zero;y' = y # zero};

Here’s the English reading of this theorem: “For all values of x, y, and st, if we run legato on these values and get the results hi and lo, then, it’ll be the case that x * y = 256 * hi + lo.” The only caveat is that we have to do arithmetic operations over 16 bit values (instead of 8), to make sure the theorem statement correctly captures the intended mathematical meaning. (Recall that all Cryptol arithmetic is modular with respect to the bit-size involved.) Hence, we simply add extra zero‘s at the end to enlarge the arguments to 16 bits. Note that, we do not have to assert that the value of lo is at most 255; this is automatically guaranteed by the fact that it is an 8-bit value. Cryptol’s bit-precise type system saves the day!

Verification

Here’s what happens when I run cryptol on the file containing the above theorem:

$ cryptol legato.cryCryptol version 1.8.5, Copyright (C) 2004-2009 Galois, Inc.www.cryptol.netType :? for helpLoading "legato.cry".. Checking types.. Processing.. Done!*** Auto quickchecking 1 theorem.*** Checking "legatoIsCorrect" ["legato.cry", line 147, col 1]Checking case 100 of 100 (100.00%)100 tests passed OK[Coverage: 3.47e-14%. (100/288230376151711744)]

When Cryptol sees a theorem declaration in a loaded file, it automatically performs a quick-check run to provide feedback on its validity. In this case, Cryptol automatically created 100 random test values for the theorem and checked that each one of them satisfied the statement. This is a quick way of getting feedback on the correctness of theorems, courtesy of Cryptol at no additonal cost to the user!While the quick-check run is promising, the coverage info indicates that we’ve barely scratched the surface. The entire state space in this case has 58 bits (8 each for x and y, plus the starting arbitrary state of the Mostek machine costing us an extra 42 bits; for a total of 58). The total number of possible inputs is, therefore, 2⁵⁸ or 288230376151711744. This is a huge number: If you had a computer that run 1-billion (10⁹) test cases every second, it’d still take you over 9 years to go through all possible inputs!Of course, we can do better. Cryptol’s theorem proving environment uses modern equivalence-checkers to prove such theorems automatically, at the push of a (virtual) button:

 legato> :prove legatoIsCorrectQ.E.D.

And there, we’ve proved that our implementation of Legato’s multiplier is indeed correct for all possible inputs! (The above proof takes about 2.5 minutes to complete on my 3-year old MacBook Pro, using abc as the underlying equivalence checker in Cryptol’s symbolic mode. I should also note that the symbolic mode is only available in the full Cryptol release, for which free licenses are available.)

Closing thoughts

I must emphasize that we are not advocating Cryptol as a platform for doing proofs of algorithm correctness. Modern theorem provers such as ACL2, Coq, or Isabelle are the leading tools in this regard. (In particular, the logic behind Cryptol’s automated theorem prover is much less expressive, for starters.) Where Cryptol shines is in its restricted attention to bit-vectors and data-flow algorithms (cryptography being a prime application area), and it turns out that automated equivalence-checking based techniques do perform rather well for such problems. Our shallow embedding of Legato’s multiplier and the automated proof-of-correctness is a case in point.There is one more important point to make. While push-button provers are indispensable in industrial practice, the final Q.E.D. you get from an interactive theorem prover such as ACL2 or Isabelle is much more satisfactory. For instance, we can hardly claim that the above proof increased our understanding of Legato’s algorithm in any sense, it just made us really believe it. I’m willing to bet that anyone who goes through a similar proof in ACL2 or Isabelle would have a much higher chance of having their “aha!” moment, where everything just sinks in…On the practical side, however, nothing beats the fully-automated Q.E.D., especially when your boss is breathing down your neck!

Download

The Cryptol file containing Legato’s multiplier and the correctness theorem is here. The Cryptol toolset licenses are freely available at www.cryptol.net.

The July 7th Galois Tech Talk will be delivered by Ivan Sutherland, titled “The Fleet Architecture”

• Date: Tuesday, July 7th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Slides are now available.Abstract: This talk describes a radically different architecture for computing called Fleet. Fleet accepts the limitations to computing imposed by physics: moving data around inside a computer costs more energy, more delay, and more chip area than the arithmetic and logical operations ordinarily called “computing.” Fleet puts the programmer firmly in charge of the most costly resource, communication, instead of in charge of the arithmetic and logical resources that are now almost free. Fleet treats arithmetic and logical operations as side effects of where the programmer sends data.Fleet achieves high performance through fine grain concurrency. Everything Fleet does is concurrent at the lowest level; programmers who wish sequentiality must program it explicitly. Fleet presents a stark contrast to today’s multi-core machines in which programmers seek concurrency in an inherently sequential environment.The Fleet architecture uses a uniform switch fabric to simplify chip design. A few thousand identical copies of a programmable interface connect a thousand or so repetitions of basic arithmetic, logical, input-output, and storage units to the switch fabric. The uniform switch fabric and its identical programmable interfaces replace many of the hard parts of designing the computing elements themselves.Both software and FPGA simulators of a Fleet system are available at UC Berkeley. Berkeley students have written a variety of Fleet programs; their work helped to define what the programmable interface between computing and communication must do. A simple compiler now produces the programs required at source and destination to provide flow-controlled communication. We expect work on a higher-level language to appear soon as a PhD dissertation.A recent 90 nanometer TSMC test chip, called Infinity, demonstrated switch fabric performance at about 4 GHz. A new test chip, called Marina, has just gone out for fabrication. Marina will test the programmable interface, and if successful, will give us confidence to build a complete Fleet. We seek participation from sponsors, programmers, and designers of basic computation elements.Bio: Ivan Sutherland is a Visiting Scientist at Portland State University where he and Marly Roncken have recently established the “Asynchronous Research Center” (ARC). The ARC occupies both physical and intellectual space half way between the Computer Science (CS) and Electrical and Computer Engineering (ECE) departments at the university. The ARC seeks to free designers from the tyranny of the clock by developing better tools and teaching methods for design of self-timed systems. Prior to moving to Portland, Ivan spent 25 years as a Fellow and Vice President at Sun Microsystems. A graduate of Carnegie Tech, Ivan got his PhD at MIT in 1963 and has taught at Harvard, University of Utah, and Caltech.Dr. Sutherland received the 1988 Turing Award, for his pioneering work in the field of computer graphics.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

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: www.galois.com.

The June 30th Galois Tech Talk will be delivered by Brian Huffman, titled “Verifying Stream Fusion with Isabelle/HOLCF”

• Date: Tuesday, June 30th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Slides from the talk.Abstract: Stream fusion is a system for removing intermediate data structures from Haskell programs that manipulate lists.  Formal verification of such libraries requires very precise modeling in a theorem prover, to avoid strictness-related bugs.In this talk I will present a formalization of the stream fusion library in Isabelle/HOLCF, a theorem proving environment designed especially for reasoning about functional programs.  I will show how to prove the correctness of various stream functions using “fixed-point induction”, a powerful reasoning principle for general recursive functions.Bio: Brian Huffman is a PhD student in Computer Science at Portland State  University, working with advisor John Matthews. He studies formal reasoning with  the Isabelle theorem prover, specializing in formalized mathematics and semantics of functional languages. He is currently the maintainer of Isabelle/HOLCF, a logic for domain theory.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The June 23rd Galois Tech Talk will be delivered by John Launchbury, titled “A Newbie’s Exploration of Separation Logic.”

• Date: Tuesday, June 23rd, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: I was just privileged to be in a Separation Logic Tutorial, given by its inventor, John Reynolds. Separation logic allows descriptions of storage and other resources concisely, providing a novel system for reasoning about imperative programs with shared mutable data structures. Recent years have seen a flurry of activity in Separation Logic, extending it to apply from shared-variable concurrency to permission based access control mechanisms. In this informal chalk-talk I will introduce the basics of Separation Logic, providing an overview of the fundamental notions of proof techniques.Bio: John Launchbury is the CTO of Galois, Inc. Prior to founding Galois in 1999, John conducted research and instructed in Computer Science and Engineering at the Oregon Graduate Institute School of Science and Engineering at OHSU. John received First Class Honors in Mathematics from Oxford University in 1985. He holds a Ph.D. in Computing Science from University of Glasgow and won the British Computer Society’s distinguished dissertation prize.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

The June 16th Galois Tech Talk will be delivered by Trevor Elliott, titled “Orc in Haskell.”

• Date: Tuesday, June 16th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.421 SW 6th Ave. Suite 300(3rd floor of the Commonwealth Building)Portland, OR 97204

Abstract: Concurrency is difficult to realize successfully. The Orc language tackles this problem by introducing explicit concurrency as part of its core. It presents a clean, and somewhat monadic, style of programming that should look familiar to Haskell users. I will give a quick introduction to the Orc language, using several examples to motivate its use. Following this introduction, a monadic Haskell embedding of the major features will be presented, bringing a type system to Orc.Bio: Trevor Elliott is a member of the technical staff at Galois, Inc.  His interests center around functional programming, and the effective use of type systems.Slides are available for download.Update: the source is now available on Hackage (though changed from the version presented at this talk).

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.