Program Agenda

Visible to the public 

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
Tim Fraser (DARPA)

Keynote Presentation:
Building Privacy-Aware Computing Systems: An Overview of Current Capabilities and Technical Challenges

Shantanu Rane (PARC)

1000 - 1015

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 cyptography: a programming language perspective
Giles Barth (IMDEA)
1015 - 1030
1030 - 1045 Break Break Poster Session
1045 - 1100

1100 - 1115

Verifiable C: proving functional correctness of C programs in Coq, e.g. SHA-256 and HMAC
Andrew Appel (Princeton)
Software Defenses Inspired by Biodiversity
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 - 1230 Lunch (on your own)
1230 - 1245
1245 - 1300
1300 - 1315
1315 - 1330

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 Title TBD
Rebecca Richards (NSA)

1400 - 1415

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)

1415 - 1430

1430 - 1445

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)
1445 - 1500
1500 - 1515 Multi-Language and Multi-Prover Verification with SAWScript
Aaron Tomb (Galois)
Break Poster Session
1515 - 1530

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 - 1615 Adjourn for the day Bringing Hardware Hacking to Life
Colin O'Flynn (Dalhousie University)
1615 - 1630
1630 - 1645 Adjourn for the day Private Disclosure of Information
Daniel Aranki (UC Berkeley)
1645 - 1700
1700 Conference adjourned

Conference Archives: 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014