Tuesday
Oct132009

Domain Specific Languages for Domain Specific Problems

We have a new position paper on the use of EDSLs and Haskell for tackling the ``programmability gap'' of emerging high performance computing architectures -- such as GPGPUs. It will be presented tomorrow at LACSS in Santa Fe. (Download) :: PDFSlides for the talk, including a 10 minute guide to EDSLs in Haskell, and a 10 minute guide to multicore programming in Haskell, can be found here :: PDF.

Domain Specific Languages for Domain Specific ProblemsDon Stewart, Galois.Workshop on Non-Traditional Programming Models for High-Performance Computing, LACSS 2009.

As the complexity of large-scale computing architecture increases, the effort needed to program these machines efficiently has grown dramatically. The challenge is how to bridge this ``programmability gap'', making the hardware more accessible to domain experts. We argue for an approach based onexecutable embedded domain specific languages (EDSLs)---small languages with focused expressive power hosted directly in existing high-level programming languages such as Haskell. We provide examples of EDSLs in use in industry today, and describe the advantages EDSLs have over general purpose languages in productivity, performance, correctness and cost.Thanks to Magnus Carlsson, Dylan McNamee, Wouter Swiestra, Derek Elkins and Alex Mason for feedback on drafts.

Click to read more ...

Tuesday
Oct062009

Tech Talk: Constructing A Universal Domain for Reasoning About Haskell Datatypes

The October 13th Galois Tech Talk will be delivered by Brian Huffman, titled “Constructing a Universal Domain for Reasoning About Haskell Datatypes."

  • Date: Tuesday, October 13th, 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: Existing theorem prover tools do not adequately support reasoning about general recursive datatypes. Better support for such datatypes would facilitate reasoning about a wide variety of real-world programs, including those written in continuation-passing style, that are beyond the scope of current tools.This paper introduces a new formalization of a universal domain that is suitable for modeling general recursive datatypes. The construction is purely definitional, introducing no new axioms. Defining recursive types in terms of this universal domain will allow a theorem prover to derive strong reasoning principles, with soundness ensured by construction.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.

Click to read more ...

Tuesday
Sep292009

Tech Talk: Roll Your Own Test Bed for Embedded Real-Time Protocols: A Haskell Experience

The October 6th Galois Tech Talk will be delivered by Lee Pike, titled Roll Your Own Test Bed for Embedded Real-Time Protocols: A Haskell Experience"[Note: Lee has recently presented this talk at the Haskell Symposium'09 in Edinburgh. Further info and downloadable artifacts are available at his personal web-site.]

  • Date: Tuesday, October 6th, 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: We present by example a new application domain for functional languages: emulators for embedded real-time protocols. As a case-study, we implement a simple emulator for the Biphase Mark Protocol, a physical-layer network protocol in Haskell. The surprising result is that a pure functional language with no built-in notion of time is extremely well-suited for constructing such emulators. Furthermore, we use Haskell's property-checker QuickCheck to automatically generate real-time parameters for simulation. We also describe a novel use of QuickCheck as a probability calculator for reliability analysis. Bio: Lee Pike is a member of the technical staff at Galois. Previously, he was a research scientist with the NASA Langley Formal Methods Group, primarily involved in the SPIDER project. His research interests include applying formal methods to safety-critical and security-critical applications, with a focus on industrial-scale endeavors.
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.

Click to read more ...

Thursday
Sep102009

Tech Talk: Building Systems That Enforce Measurable Security Goals

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.

Click to read more ...

Monday
Aug242009

Substitution ciphers in Cryptol

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.

Click to read more ...