Tech Talk: John Launchbury presents Conal Elliott’s “Beautiful Differentiation”

The December 15th Galois Tech Talk will be delivered by John Launchbury.  He will present Conal Elliott’s 2009 ICFP paper entitled  Beautiful Differentiation for those of us who were not able to attend this wonderful talk in-person.

  • Date: Tuesday, 10:30am, 15 Dec 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: Automatic differentiation (AD) is a precise, efficient, and convenient method for computing derivatives of functions. Its forward-mode implementation can be quite simple even when extended to compute all of the higher-order derivatives as well. The higher-dimensional case has also been tackled, though with extra complexity. This paper develops an implementation of higher-dimensional, higher-order, forward-mode AD in the extremely general and elegant setting of calculus on manifolds and derives that implementation from a simple and precise specification.In order to motivate and discover the implementation, the paper poses the question, “What does AD mean, independently of implementation?‚” An answer arises in the form of naturality of sampling a function and its derivative. Automatic differentiation flows out of this naturality condition, together with the chain rule. Graduating from first-order to higher-order AD corresponds to sampling all derivatives instead of just one. Next, the setting is expanded to arbitrary vector spaces, in which derivative values are linear maps. The specification of AD adapts to this elegant and very general setting, which even simplifies the development.Bio: John Launchbury is the founder and Chief Scientist of Galois, Inc.


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.

Read More

Tech Talk: Hoare-Logic – fiddly details and small print

[Note the Friday date, instead of the usual Tuesday slot.]The November 13th Galois Tech Talk will be delivered by Rod Chapman, titled Hoare-Logic – fiddly details and small print.”

  • Date: Friday, November 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: Hoare’s “assignment axiom” is noted for its simplicity and elegance, which seems to suggest that practical implementations are somehow “easy”. This talk will focus on our experience with SPARK – a programming language and toolset whose principal design goal is the provision of a sound Hoare-style verification system. I will concentrate on the “small print” and various fiddly (but essential) langauge features, such as volatility, I/O, dealing with commercial compilers, soundness and so on, that make the system much harder to implement than you might think.Bio: Rod Chapman is a Principal Engineer with Praxis, specializing in the design and implementation of safety and security-critical systems. He currently leads the development of the SPARK language and its associated analysis tools.Rod is a well-known conference speaker and has presented papers, tutorials, and workshops at many international events including SSTC, NSA HCSS, SIGAda, Ada-Europe and the Society of Automotive Engineers (SAE) World Congress. In addition to SPARK, Rod has been the key contributor to many of Praxis’ major projects such as SHOLIS, MULTOS CA, Tokeneer and Software verification tools. He received a MEng in Computer Systems and Software Engineering and a DPhil in Computer Science from the University of York, England, in 1991 and 1995 respectively. He is a Chartered Engineer, a Fellow of the British Computer Society, and also an SEI-Certified PSP Instructor.


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.

Read More

Tech Talk: Testing First-Order-Logic Axioms in AutoCert

The November 3rd Galois Tech Talk will be delivered by Ki Yung Ahn, titled “Testing First-Order-Logic Axioms in AutoCert.”

  • Date: Tuesday, November 3rd, 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: AutoCert is a formal verification tool for machine generated code in safety critical domains, such as aerospace control code generated from MathWorks Real-Time Workshop.  AutoCert uses Automated Theorem Proving (ATP) systems based on First-Order-Logic (FOL) to formally verify safety and functional correctness properties of the code.  These ATP systems try to build proofs based on user provided domain-specific axioms, which can be arbitrary First-Order-Formulas (FOFs).  That is, these axioms are the crucial trusted base in AutoCert.  However, formulating axioms correctly (i.e.  precisely as the user had really intended) is non-trivial in practice, and speculating validity of the axioms from the ATP systems is very hard since theorem provers do not give examples or counter-examples in general.We adopt the idea of model-based testing to aid axiom authors to discover errors in axiomatization.  To test the validity of axioms, users can define a computational model of the axiomatized logic by giving interpretations to each of the function symbols and constants as computable functions and data constants in a simple declarative programming language.  Then, users can test axioms against the computational model with widely used software testing frameworks.  The advantage of this approach is that the users have a concrete intuitive model with which to test validity of the axioms, and can observe counterexamples when the model does not satisfy the axioms.  We have implemented a proof of concept tool using Template Haskell, QuickCheck, and Yices.(This is a joint work with Ewen Denney at SGT/ NASA Ames Research Center, going to be presented in the poster session at Asian Symposium on Programming Languages and Systems this December.)Bio: Ki Yung Ahn is a Ph.D student at Portland State University working with Tim Sheard and other members of the TRELLYS project, designing and implementing a dependently typed programming language that is general purpose programming friendly. He received a BS in Computer Science from KAIST in 2002, worked as online storage service server programmer at Gretech before joining graduate program at Portland State University in 2005.  He has been working on Shared Subtypes, Korean translation of “Programming in Haskell” by Graham Hutton, and enjoying other small funs of Haskell hacking.


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.

Read More

Tech Talk: How to choose between a screwdriver and a drill

The October 27th Galois Tech Talk will be delivered by Tanya Crenshaw, titled “How to choose between a screwdriver and a drill.”

  • Date: Tuesday, October 27th, 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: Suppose you have two different algorithms to compute the same result. One is clearly safe. It is simple enough to verify. The other has more desirable features, but it is too complicated to verify. You want a system that can choose between these two algorithms while meeting its quality of service goals. This is the intuition behind Lui Sha’s Simplex Architecture. The intuition is simple, but its verification is not. Implementations of the Simplex Architecture are reactive systems whose properties are not always easy to express. In this talk, I’ll describe the history of Simplex, the challenges of verifying its safety properties, and a variety of approaches to modeling it, from an architecture description language to an executable specification language.Bio: Tanya L. Crenshaw is an assistant professor of computer science at the University of Portland. She teaches courses in both Computer Science and Electrical Engineering and conducts research into security for embedded systems. Before University of Portland, she worked for Wind River and Sharp Microelectronics and studied at the University of Illinois at Urbana-Champaign where she completed her Ph.D. (Her personal web-page is at: http://kaju.dreamhosters.com/.)


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.

Read More

Tech Talk: Writing Linux Kernel Modules with Haskell

The October 20th Galois Tech Talk will be delivered by Thomas DuBuisson, titled “Writing Linux Kernel Modules with Haskell.”

  • Date: Tuesday, October 20th, 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 for this talk are now available.Abstract: Current operating systems are developed and extended primarily with imperative languages that lack in expressiveness and safety.  Pure and functional languages fill these gaps nicely but existing tools are not ideal fits and the language abstracts away important environmental information.This talk will focus on modifications of the Glasgow Haskell Compiler to generate suitable code and nuances of binding to the Linux API. Short-comings of the language and tools will be identified along with known workarounds and potential engineering efforts.Bio: Thomas DuBuisson is a PhD student in Computer Science at Portland State University, working with advisor Andrew Tolmach.  Current research efforts revolve around the use of functional languages for systems programming and improving runtime system security.


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.

Read More

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.

Read More

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.

Read More

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.

Read More

Tech talk: Programming the fleet

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.

Read More

Tech Talk: Mathematics of Cryptography: A Guided Tour

Tuesday, July 28, 2009

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.

Read More