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