Tech Talk: Hardware Security's Hierarchy of Attacks

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Hardware Security's Hierarchy of Attacks

speaker: Joe FitzPatrick

time: Tuesday, 30 April 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

Generally, there is a very low barrier to entry when it comes to software or network-based attacks due to the fact that actual costs are minimal and most resources are readily available. This does mean that it's generally much easier to attack the software of a system than the hardware, but unfortunately that also leads to overconfidence in, as well as misplaced trust in hardware.

There is a clear 'hierarchy of attacks' in the hardware world. There are costs, often significant, involved in acquiring your hardware 'target' which might be damaged or destroyed in the process. There are a number of useful tools that cost anywhere from a few dollars to a few million dollars. I'll give a couple examples of what's possible within budgets of $100, $10,000, and $1,000,000. I'll point out how many capabilities are much more accessible than most assume, and how vulnerable to sub-$100 attacks most of our 'secure' hardware really is.

bio:

Joe FitzPatrick is an independent hardware security consultant and trainer. He spent 8 years validating and debugging desktop and server CPUs, including hardware penetration testing and security validation training for functional validators worldwide. He is currently developing a week-long hands-on workshop focused on low cost hardware security attacks.

Galois Working with SRI on Trustworthy Mobile Device for USMC

SRI announced this week that, with Galois' help, it is beginning final development of a trusted mobile device for the U.S. Marine Corps. Galois is pleased to be working with SRI on improving the trustworthiness of commercial mobile phones. Read more about it here.

Tech Talk: Introducing HERMIT, a Plugin for Transforming GHC Core Language Programs

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Introducing HERMIT: A Plugin for Transforming GHC Core Language Programs

speaker: Andrew Farmer

time: Tuesday, 09 April 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks, leaving the programmer to do them by hand. This talk introduces HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them. The talk will explore design choices in HERMIT, demonstrate its use on examples, and seek input for further development and case studies.

bio:

Andrew Farmer is a Ph.D. student at the University of Kansas, working with Andy Gill. He received his B.S. in Computer Science from the University of Kansas in 2005 and went off to industry to write domain specific languages for web application development. Returning to KU in the fall of 2009, Andrew's interests include programming language design in general and specifically the compilation and optimization of functional languages. He has done work on testing and debugging tools for the Kansas Lava project. He is currently working on the HERMIT project, where he is interested in leveraging HERMIT's capabilities to write domain-and-program-specific optimizers.

Tech Talk: Inferring Phylogenies Using Evolutionary Algorithms

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Inferring Phylogenies Using Evolutionary Algorithms

speaker: Erlend Hamberg

time: Tuesday, 12 March 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

An important problem in genetics is phylogenetic inference: Coming up with good hypotheses for the evolutionary relationship between species – usually represented as a “family tree”. As the amount of molecular data (e.g. DNA sequences) quickly grows, efficient algorithms become increasingly important to analyze this data. A maximum-likelihood approach with models for nucleotide evolution allows us to use all the sequence data, but is a computationally expensive approach. The number of possible trees also grows rapidly as we include more species. It is therefore necessary to use heuristic search methods to find good hypotheses for the “true” tree. Evolutionary algorithms (EA) is a class of such search/optimization algorithms that has been shown to perform well in other areas where the search space is large and irregular. I will explain my approach and my findings from using an evolutionary algorithm for inferring phylogenies from molecular data.

bio:

Erlend Hamberg obtained his M.Sc. in Computer Science from the Norwegian University of Science and Technology (NTNU) in 2011. For his Master's thesis research he worked on the problem of inferring phylogenies (i.e. the evolutionary relationship between species) from molecular data. He was previously at ARM where he worked on the drivers for Mali series of GPUs.

Tech Talk: Parametricity, Quotient types, and Theorem transfer

Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)

title: Parametricity, Quotient types, and Theorem transfer

speaker: Brian Huffman

time: Tuesday, 05 March 2013, 10:30am.

location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract:

A polymorphic function may be instantiated at many different types; if the function is parametrically polymorphic, then all of its instances must behave uniformly. Reynolds' parametricity theorem expresses this precisely, in terms of binary relations derived from types. One application of the parametricity theorem is to derive Wadler-style "free theorems" about a polymorphic function from its type; e.g. rev :: [a] -> [a] must satisfy map f (rev xs) = rev (map f xs).

In this talk, I will show how to apply many of the ideas behind parametricity and free theorems in a new setting: formal reasoning about quotient types. Using types-as-binary-relations, we can automatically prove that corresponding propositions about quotient types and their representation types are logically equivalent. This design is implemented as the Transfer package in the Isabelle theorem prover, where it is used to automate many proofs about quotient types.

bio:

Brian Huffman is a recent PhD graduate from the Department of Computer Science at Portland State University, now at Galois after completing a postdoc at the Technical University of Munich. He has been an avid Haskell programmer since 2001, and has contributed to the development of the Isabelle interactive theorem prover since 2005, with an emphasis on tools for verifying lazy functional programs. Several of Brian's formalizations can be found online at the Archive of Formal Proofs.