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