| |
TUESDAY, MAY 5
Proof Engineering |
WEDNESDAY, MAY 6
Sustainable Integrity
|
THURSDAY, MAY 7
Privacy
|
| 0900 - 1000 |
Keynote Presentation:
Proof Engineering: The Soft Side of Hard Proof
Gerwin Klein (NICTA) |
Keynote Presentation:
Detecting Malice in Commodity Software
Tim Fraser (DARPA) |
Keynote Presentation:
Building Privacy-Aware Computing Systems: An Overview of Current Capabilities and Technical Challenges
Shantanu Rane (PARC) |
| 1000 - 1030 |
Cerberus: Towards an Executable Semantics for Sequential and Concurrent C11
Kayvan Memarian
(University of Cambridge) |
Remote Attestation for Cloud-Based Systems
Perry Alexander
(University of Kansas) |
Reconciling Provable Security and Practical Cryptography: A Programming Language Perspective
Gilles Barth (IMDEA) |
| 1030 - 1100 |
BREAK |
BREAK |
POSTER SESSION |
| 1100 - 1115 |
Verifiable C: proving functional correctness of C programs in Coq, e.g. SHA-256 and HMAC
Andrew Appel (Princeton) |
Biologically Inspired Software Defenses
Michael Franz (UC Irvine) |
| 1115 - 1130 |
A Cut Principle for Information Flow
Joshua Guttman
(The MITRE Corporation and WPI) |
| 1130 - 1145 |
Deep Specifications and Certified Abstraction Layers
Ronghui Gu (Yale) |
Not-quite-so-broken TLS: Lessons in Re-engineering a Security Protocol Specification and Implementation
David Kaloper Mersinjak
(Univ. of Cambridge) |
| 1145 - 1200 |
Models and Games for Quantifying Vulnerability of Secret Information
Piotr Mardziel (University of MD) |
| 1200 - 1215 |
LUNCH
(on your own) |
LUNCH
(on your own) |
| 1215 - 1330 |
LUNCH
(on your own) |
| 1330 - 1345 |
Qualification of Formal Methods Tools
Darren Cofer (Rockwell Collins) |
Rigorous Architectural Modelling for Production Multiprocessors
Shaked Flur, Kathryn Gray, Christopher Pulte
(University of Cambridge) |
| 1345 - 1400 |
NSA Civil Liberties & Privacy: Bridging the Art and Science of Privacy
Rebecca Richards (NSA) |
| 1400 - 1430 |
Issues, Challenges and Opportunities in the Qualification of Formal Method Tools
Cesare Tinelli (University of Iowa) |
A Formal Specification of x86 Memory Management
Shilpi Goel and Warren Hunt
(UT Austin) |
| 1430 - 1500 |
BREAK |
Language-based Hardware Verification with ReWire: Just Say No! to Semantic Archaeology
William Harrison
(University of Missouri) |
High Assurance Cryptography Synthesis with Cryptol
Joseph Kiniry (Galois) |
| 1500 - 1530 |
Multi-Language and Multi-Prover Verification with SAWScript
Aaron Tomb (Galois) |
BREAK |
POSTER SESSION |
| 1530 - 1545 |
CodeHawk: Sound Static Analysis for Proving the Absence of Memory Related Software Vulnerabilities
Douglas Smith (Kestrel Technology) |
Achieving High Speed and High Assurance in a Hardware-Based Cross-Domain System Using Guardol
David Hardin (Rockwell Collins) |
| 1545 - 1600 |
Privacy through Accountability
Anupam Datta
(Carnegie Mellon University) |
| 1600 - 1630 |
Adjourn for the day |
Bringing Hardware Hacking to Life
Colin O'Flynn (Dalhousie University) |
| 1630 - 1700 |
Adjourn for the day
|
Private Disclosure of Information
Daniel Aranki (UC Berkeley) |
| 1700 |
Conference adjourned |
| 1830 |
Conference Dinner
The Chart House
300 2nd Street
Annapolis, MD 21401
|
