SecDev is a venue for presenting ideas, research, and experience about how to develop secure systems. It focuses on theory, techniques, and tools to “build security in” to existing and new computing systems, and does not focus on simply discovering the absence of security.
The goal of SecDev is to encourage and disseminate ideas for secure system development among academia, industry, and government. It aims to bridge the gap between constructive security research and practice and to enable the real-world impact of security research in the long run. Developers have valuable experiences and ideas that can inform academic research, and researchers have concepts, studies, and even code and tools that could benefit developers.
SecDev 2019 will feature keynote speakers June Andronick of UNSW and The Commonwealth Scientific and Industrial Research Organisation (CSIRO) and Colm MacCárthaigh of Amazon Web Services. Below, they offer details on their featured research:
“Componentise, Isolate, Prove: The seL4 Security Story” by June Andronick
“Is formally verified software more secure? Well, it depends: more secure than what? If a software system is secure already, then formal verification simply supplies the evidence (and in fact the strongest possible evidence) that it actually is secure. Most developed software systems, however, even when built with security in mind, will inevitably still contain errors that lead to vulnerabilities. The process of providing a formal proof of the system’s security will reveal these vulnerabilities, and it reveals all of them — as opposed to testing (as long as you can clearly define what security means, of course). In the extreme case where the system has no built-in security, then formal verification is not of much help to magically add security as an afterthought; it cannot, for instance, suggest a redesign of the implementation.
“In this talk I’ll present the approach we advocate for building software that is provably secure, and I will give evidence of its success, and of its impact on systems that have been built on our formally verified seL4 microkernel.”
June Andronick leads the Trustworthy Systems group, world-leading in verified operating systems software, known worldwide for the formal verification of the seL4 microkernel. She is a Principal Research Scientist at Data61|CSIRO, and conjoint Associate Professor at UNSW Sydney, Australia.
“Baking the Best Security Layer-Cake” by Colm MacCárthaigh
“On the Amazon s2n team, we have a rule for handling bugs and issues; it’s not good enough to simply fix a bug or issue, we also have to dig in and find another deeper kind of fix that eliminates most bugs of that whole class. Failsafe design and defense in depth is nothing new of course, but in security, the tendency to add layers can backfire. Each new layer brings its own potential bugs, risks, costs, and challenges. No good deed goes unpunished! But there is hope. We’re getting more experienced and better at sniffing out risk, and seeing just how valuable different kinds of defense are. We’ll take a look at just how effective some of the simplest mitigations are, and how modern verification techniques can provide run-time assurance, without run-time risk.”
Colm MacCárthaigh is a senior principal engineer at Amazon Web Services, where for the last 11 years he has been working on many of Amazon’s core security, networking, and cryptography services. For the last 5 years, Colm has been leading the development of Amazon s2n, an Open Source implementation of the SSL/TLS protocols, and has been applying Formal Verification, Automated Reasoning, and secure code generation techniques to eliminate as many potential issues as possible.