Tech Talk: Towards a High-Assurance Runtime System: Certified Garbage Collection

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.
Read More

Tech Talk: Coverset Induction with Partiality and Subsorts: A Powerlist Case Study

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study
presenter:
Joe Hendrix
time:
10:30am, Tuesday, 22 June 2010.
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:

Many inductive theorem provers use induction schemes derived from the recursive calls in functions definitions. This widely-used strategy is called coverset induction in the context of algebraic specifications. One challenge in applying coverset induction is that it typically requires using a total recursive function, while many operations on data structures are only meaningful on some well-formed subset of their possible inputs.

In this talk, I’ll discuss a generalization of coverset induction to handle partial constructors and operations. The generalization is implemented in the Maude ITP, and used in an extensive case study involving powerlists — a data structure introduced by J. Misra to elegantly formalize parallel algorithms based on divide and conquer strategy. Powerlists are constructed by partial operations, and it has been a challenge to naturally reason about powerlists using a formal logic that only supports total operations. We show how theorems about powerlists can be elegantly proven using the generalized coverset induction scheme implemented in the Maude ITP.

bio:
Joe is a member of the technical staff at Galois, Inc. He is interested in developing tools for making software development easier and safer. He started out developing software for civil engineers to analyze the safety of bridge foundations. He worked on automated decision procedures during his PhD at the University of Illinois. Immediately prior to joining Galois, he developed software within Microsoft’s Trustworthy Computing Initiative.
Read More

Tech Talk: Introducing Well-Founded Recursion

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.
Read More

Tech Talk: Large-Scale Static Analysis at Mozilla

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!

title:
Large-Scale Static Analysis at Mozilla (slides, video)
presenter:
Taras Glek
time:
10:30 am, 8 June 2010, Tuesday
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
A competitive browser market requires fast-paced improvements to the codebase. Such improvements may require significant refactoring of large parts of the codebase. Mozilla Firefox is one of the largest open source C++ projects. Unfortunately C++ is a complex language: method overloading, virtual functions, template instantiation, pointer arithmetic, etc reduce developer productivity. Mozilla developed C++ static analysis and refactoring tools to increase developer leverage in C++. Static analysis is done via Dehydra/Treehydra GCC plugins and refactoring is accomplished by extending the Elsa C++ parser. This talk will discuss why Mozilla needs static analysis, why there are so few tools for C++, and specific projects that we’ve embarked on.
bio:
Taras Glek is a software engineer at Mozilla Corporation. He works on static analysis and startup performance. Taras blogs about it at http://blog.mozilla.com/tglek/.
Read More

Tech Talk: Categories are Databases

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 Thursday.

title:
Categories are Databases (slides, video)
presenter:
Dr. David Spivak
time:
10:30 am, 03 June 2010, Thursday
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
Category theory is a powerful language for organizing layers of abstraction in all areas of mathematics. Databases are powerful tools for organizing information of all sorts. Whereas categories are often considered hopelessly abstract, databases are often considered horrifically mundane. Thus it is either strange or fitting that, mathematically speaking, categories and databases are the same concept. In this talk I’ll show how to turn any database into a category and any category into a database. I’ll also discuss functors and how they may be useful for issues of data migration and merging.
bio:
David Spivak graduated with a PhD in mathematics from UC Berkeley in 2007; his thesis used higher category theory to fix an old problem in geometry. From 2007 to the present, he have been a postdoc at the University of Oregon in the Math Department. During this time, his focus has moved toward the idea of using category theory to understand information and communication.  This summer, he will become a mathematics postdoc at MIT for three years, focusing on information and communication from a category-theoretic perspective.
Read More

Tech Talk: The L4.verified Project

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.
Read More

Tech Talk: Developing Good Habits for Bare-Metal Programming

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.
Read More

Tech Talk: Typing Directories

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!The talk will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)


Typing DirectoriesDetails:

  • Presenter: Kathleen Fisher, AT&T Labs
  • Date: Monday May 03, 2010
  • Time: 3:30pm (NOTE THE CHANGED DATE AND TIME!)

Abstract: PADS describes the contents of individual ad hoc data files, but has no provisions for describing collections of files, i.e., directories. In this talk, I explore examples where having a declarative description of directories as well as files would be useful, including websites, source code trees, source code control systems, operating systems, and scientific data sets. As part of this exploration, I identify essential features of a directory description language and useful tools that might be produced from such a description. I end with a series of questions about how such a language might most easily be implemented in the context of Haskell.This is joint work with David Walker and Kenny Zhu.Bio: (from http://www.research.att.com/people/Fisher_Kathleen_S) Kathleen Fisher is a Principal Member of the Technical Staff at AT&T Labs Research and a Consulting Faculty Member in the Computer Science Department at Stanford University.  Kathleen’s research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management.  The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data, including the Hancock system for efficiently building signatures from massive transaction streams and the PADS system for managing ad hoc data.Kathleen is an ACM Distinguished Scientist.  She has served as program chair for FOOL, CUFP, and ICFP. She is past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN), Co-Chair of CRA’s Committee on the Status of Women (CRA-W), and an editor of the Journal of Functional Programming.  She is currently serving on the CRA Board.

Read More

Tech Talk: Visualizing Information Flow through C Programs

Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!The talk will be held atGalois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)


Visualizing Information Flow through C Programs (slides)

Details:

  • Presenter: Joe Hurd
  • Date: Tuesday April 27, 2010
  • Time: 10:30am

Abstract: The aim of the Automated Security Analysis project is to determine whether the information flows in a realistically-sized C codebase can be automatically deduced and communicated in an understandable way to someone unfamiliar with the code. To test this, a new information flow static analysis and visualization technique were developed, and implemented in a research prototype tool. This talk will present the novel features of the static analysis and demonstrate how the results are shown in the visualization tool: information flow between program storage locations is decomposed into two compositional properties, which can be computed using sound abstract interpretation techniques. For each deduced information flow, the static analysis keeps track of a set of source code locations which demonstrate the information flow, and this is used by the visualization component to communicate the information flow to a user browsing the source code.

Bio: Joe Hurd, Ph.D. is a Formal Methods Engineer at Galois, Inc. For the past ten years Dr. Hurd has been applying theorem proving techniques to formally verify the correctness of complex software, including probabilistic programs, elliptic curve cryptography and game tree analysis algorithms. He is also the developer of Metis, an automatic theorem prover for first order logic, and coordinates the OpenTheory project, a package management system for higher order logic theories. Dr. Hurd is an active member of the theorem proving research community, having organized conferences in 2005 and 2008, given invited talks, and regularly appears on program committees and reviews papers for conferences and journals. Prior to joining Galois in 2007, Dr. Hurd was a research fellow at Magdalen College, University of Oxford. He studied at the University of Cambridge, receiving a Masters level degree in Mathematics in 1997, and a Ph.D. in Computer Science in 2002.

Read More