Thursday
Jun062013

Tech Talk: Non-interference and Binary Correctness of seL4

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

Please note that this talk is on Friday, at 11am

title:Non-interference and Binary Correctness of seL4

speaker:Gerwin Klein and Thomas Sewell, NICTA
time: Friday, 14 June 2013, 11:00am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code.

The first part of the talk presents a new non-interference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain.

The binary proof addresses the compiler-correctness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assembly-like programs powered by modern SMT solvers. We cover the previously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1.

bio: Thomas Sewell has worked in the verification group at NICTA for seven years as a staff engineer and Isabelle/HOL proof specialist. Thomas was part of the seL4 proof effort from the beginning, working on the functional correctness proof and later proofs of security properties. He has recently begun joint work with Magnus Myreen (Cambridge University) to work on binary verification for the compiled kernel, and has also recently enrolled at UNSW as a PhD student on this project.

Gerwin Klein is Principal Researcher at NICTA, Australia's National Centre of Excellence for ICT Research, and Conjoint Associate Professor at the University of New South Wales in Sydney, Australia. He is leading NICTA's Formal Methods research discipline and was the leader of the L4.verified project that created the first formal, machine-checked proof of functional correctness of a general-purpose microkernel implementation in 2009. He joined NICTA in 2003 after receiving his PhD from Technische Universität München,Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL.

Gerwin has won a number of awards together with his team, among them the 2011 MIT TR-10 award for the top ten emerging technologies world-wide, and NICTA's Richard E. Newton impact award for the kernel verification work.

Thursday
May302013

Tech Talk: Pi in the Sky: How Computer Vision can give a Quadcopter Autonomous Flight

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: Pi in the Sky: How Computer Vision can give a Quadcopter Autonomous Flight
speaker: A team of PSU students
time: Tuesday, 4 June 2013, 10:30am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)

abstract: Five students in PSU’s Electrical and Computer Engineering Senior Capstone sequence want to show you what they’ve created: an inexpensive computer vision system for a quadcopter running on a Raspberry Pi board. One might be surprised how simple it is to code a decent object tracking algorithm using open-source software, and how difficult it is to keep a quadcopter from crashing into the wall in the debug stage. This talk should appeal to the RC hobbyist, the embedded systems programmer, and anyone interested in the art of computer vision. The presentation will include video footage of what these students have accomplished and how they pulled it off.

Tuesday
Apr232013

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.

Friday
Apr122013

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.

Wednesday
Apr032013

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.

Page 1 ... 4 5 6 7 8 ... 49 Next 5 Entries »