SESSION + Live Q&A
Assuring Crypto Code with Automated Reasoning
Bugs in software are ubiquitous, but the impact of these bugs can vary widely. Sometimes they are largely benign, and at other times they can have catastrophic effects. Bugs in cryptographic software tend to be especially serious. To add to that, cryptographic algorithms are difficult to design and implement, requiring intricate and rare expertise. And even worse, such software operates in a context that can be assumed to be malicious, rather than random.
To achieve confidence of the correctness of cryptographic implementations in this context, we therefore need to apply a more rigorous testing standard. Ideally, we want to be able to test an implementation on all possible inputs. Fortunately, advances in automated reasoning technology, particularly in SAT and SMT solvers, makes exactly this approach possible, and even efficient.
This talk will describe the capabilities and operation of some open source tools that allow developers to conclusively and largely automatically determine whether a low-level cryptographic implementation, written in a language such as C, exactly matches a higher-level mathematical specification. We will particularly focus on work we have done to integrate these tools into the continuous integration system of Amazon's s2n implementation of TLS.
Speaker
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/aaron_tomb1.jpg?itok=CM_MuJGE)
Aaron Tomb
Research Lead, Software Correctness @Galois
Dr. Tomb received his B.S., M.S., and Ph.D. in computer science from the University of California, Santa Cruz. His academic work focused on programming language theory, and particularly on the use of advanced programming language technology to improve software reliability. This involves type...
Read moreFrom the same track
SQL Server On Linux: Will It Perform Or Not?
Will SQL Server perform on Linux better than on Windows? Have you been wondering whether the multi-layer architecture the team revealed recently will hurt SQL Server’s performance? Are you still not convinced about the entire endeavor. Come, listen to the talk, learn about SQL Server’s...
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/dsc_0002.jpg?itok=DidiQ_Co)
Slava Oks
Core Developer Behind Porting SQL Server to Linux @Microsoft
Property-Based Testing In Practice
Testing is a cornerstone of modern software development. It provides us with a safety net against bugs and regressions – without testing, it would be impossible to write large-scale applications. The traditional approach to testing relies on hard-coded examples: fire some specific inputs into...
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/alex_chan.jpg?itok=JeYwYJ7f)
Alex Chan
Hypothesis Maintainer & Software Developer @WellcomeTrust
Panel: What's Next for Our Programming Languages?
Types, testability, tooling, paradigms, productivity, managed, native, concurrency, parallelism, performance, asynchrony, integrations, memory management, security, resilience, or, maybe, simple readability? What are the important things crossing the minds of language designers today as they...
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/10094934084_2006994711.jpg?itok=8by-mZgW)
Brian Goetz
Java Language Architect @Oracle
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/joeduffy.jpg?itok=XRVczVeR)
Joe Duffy
Pulumi Co-founder & CEO, Previously @Microsoft Director of Engineering for Languages/Compilers
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/Martin%20Thompson.jpg?itok=yxNNSL8p)
Martin Thompson
High Performance & Low Latency Specialist
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/sylvan.jpg?itok=AhMFzl80)
Sylvan Clebsch
CTO @Causality
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/profille-green-shirt.jpg?itok=-quR-7yj)
Richard Feldman
Elm Pioneer & Software Engineer @noredink
Power of the Log:LSM & Append Only Data Structures
This talk is about the beauty of sequential access and append only data structures. We'll do this in the context of a little known paper entitled “Log Structured Merge Trees”. LSM describes a surprisingly counterintuitive approach to storing and accessing data in a sequential fashion. It came...
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/ben_stopford_2.jpg?itok=YzOgIoeR)
Benjamin Stopford
Author of “Designing Event Driven Systems” & Senior Director @confluentinc
Pony: Co-Designing A Type-System And A Run-Time
Pony is an actor-model, capabilities-secure, native programming language. I will talk about reference capabilities (a type system for data-race freedom influenced by object capabilities and deny guarantee reasoning), the ORCA and MAC protocols for fully concurrent no-stop-the-world garbage...
![](https://archive.qconlondon.com/sites/qcon_london/files/styles/240x240/public/sylvan.jpg?itok=AhMFzl80)
Sylvan Clebsch
CTO @Causality