In this post I discuss a program security property called noninterference. I motivate why you might like it if your program satisfied noninterference, and show that the property is fundamental to many areas beyond just security. I also explore some programming languages and tools that might help you enforce noninterference, noting that while tainting analysis won’t get you the whole way there, research tools that attempt to do better have their own problems. I conclude with some suggestions for future research, in particular with the idea that testing noninterference may be a practical approach.
Category Archives: Software Security
What is noninterference, and how do we enforce it?
Filed under Program Analysis, Software Security, Types
Formal Reasoning in PL and Crypto
In my last post, I summarized some of the topics and problems considered at a recent Dagstuhl seminar I co-organized on the Synergy between Programming Languages and Cryptography. The post surveyed how programming languages often interface with cryptography in the construction of secure systems, and in particular how they can make it easier to implement cryptography, use it, or verify its correctness.
Beyond using PLs as a tool for easier/safer use of Crypto, there is an opportunity for certain kinds of thinking, or reasoning, to cross over fruitfully between the PL an Crypto communities. In particular, both communities are interested in formalizing systems and proving properties about them but they often use different methods, either due to cultural differences, or because the properties and systems of interest are simply different. During the workshop we identified both analogous, similar styles of reasoning in two communities and connection points between the different styles of reasoning. In this post I briefly highlight a few examples of each, and point to future research opportunities.
The Synergy between Programming Languages and Cryptography
I recently had the pleasure of co-organizing a Dagstuhl Seminar on the synergy between ideas, methods, and research in programming languages and cryptography.
Dagstuhl Seminar on the Synergy between Programming Languages and Cryptography
This post and the next will summarize some interesting discussions from the seminar. In this post, I will look at how programming languages often interface with cryptography, surveying the research of the seminar participants. In my next post, I’ll dig a little deeper into one topic in particular, which is how formal reasoning in PL and Crypto compare and contrast, and how ideas from one area might be relevant to the other.
Ultimately, I came away convinced that the combination of PL and Crypto has much to offer to the problem of building secure systems.
Built, Broken, Fixed: BIBIFI Security Contest Report
Earlier in the summer I discussed a security-oriented programming contest we were planning to run called Build-it, Break-it, Fix-it (BIBIFI). The contest completed about a week ago, and the winners are now posted on the contest site, https://builditbreakit.org.
Here I present a preliminary report of how the contest went. In short: well!
We had nearly a dozen qualifying submissions out of 20 or so teams that made an attempt, and these submissions used a variety of languages — the winners programmed in Python and Haskell, and other submissions were in C/C++, Go, and Java (with one non-qualifying submission in Ruby). Scoring was based on security, correctness, and performance (as in the real world!) and in the end the first two mattered most: teams found many bugs in qualifying submissions, and at least one team was scoring near the top until other teams found their program did not pay much attention to security.
We have much data analysis still to do, to understand more about what happened and why. If you have scientific questions you think we should investigate, after reading this report, I’d love to know them. In the end, I think the contest made a successful go at emphasizing security is not just about breaking things, but also about building them correctly.
Filed under Education, Software Security
What is type safety?
In response to my previous post defining memory safety (for C), one commenter suggested it would be nice to have a post explaining type safety. Type safety is pretty well understood, but it’s still not something you can easily pin down. In particular, when someone says, “Java is a type-safe language,” what do they mean, exactly? Are all type-safe languages “the same” in some way? What is type safety getting you, for particular languages, and in general?
In fact, what type safety means depends on language type system’s definition. In the simplest case, type safety ensures that program behaviors are well defined. More generally, as I discuss in this post, a language’s type system can be a powerful tool for reasoning about the correctness and security of its programs, and as such the development of novel type systems is a rich area of research.
Filed under Dynamic languages, PL in practice, Semantics, Software Security, Types
What is memory safety?
I am in the process of putting together a MOOC on software security, which goes live in October. At the moment I’m finishing up material on buffer overflows, format string attacks, and other sorts of vulnerabilities in C. After presenting this material, I plan to step back and say, “What do these errors have in common? They are violations of memory safety.” Then I’ll state the definition of memory safety, say why these vulnerabilities are violations of memory safety, and conversely say why memory safety, e.g., as ensured by languages like Java, prevents them.
No problem, right? Memory safety is a common technical term, so I expected its definition would be easy to find (or derive). But it’s much trickier than I thought.
My goal with this post is to work out a definition of memory safety for C that is semantically clean, rules out code that seems intuitively unsafe, but does not rule out code that seems reasonable. The simpler, and more complete, the definition, the better. My final definition is based on the notion of defined/undefined memory and the use of pointers as capabilities. If you have better ideas, I’d love to know them!
Filed under PL in practice, Semantics, Software Security
How did Heartbleed remain undiscovered, and what should we do about it?
It was recently reported that the Heartbleed OpenSSL bug has still not been patched on over 300,000 servers. This is down from 600,000 that were discovered two months ago, when the bug was first publicized. Add to this delay the nearly two years that the bug went undetected, and that’s a lot of exposure.
In this blog post, I wonder about how programming languages and tools might have played a role in finding Heartbleed before it got into production code. Then I explore possible approaches to improving this state of the affairs. I welcome your thoughts and ideas! Continue reading
Filed under Formal verification, Software Security
ADS, generically, part II
This post is the second part of a post on using ideas from programming languages to assist the design of authenticated data structures (ADSs). I will describe a small programming language extension for building ADSs that I co-developed with Andrew Miller, Jonathan Katz, and Elaine Shi, called LambdaAuth. A paper on this language was presented at POPL’14 and the implementation is freely available.
As a word of warning, this post goes into some technical detail. The goal of doing so is to make, in detail, a general point: programming language researchers’ focus on ways of programming (often embodied as language features, patterns, transformations, or analyses), rather than particular programs, yields broadly applicable results, extending outside of the motivating examples or domain. In this case, LambdaAuth embodies a simple mechanism for programming any authenticated data structure, not just one particular kind.
Filed under Secure computation, Software Security, Uncategorized
Authenticated Data Structures (Generically)
This blog post is the first in my series on secure computation and will be presented in two parts. It briefly introduces some work my collaborators and I published this year, which illustrates a pleasant application of programming languages ideas to cryptographic computation.
In particular, we develop a general-purpose technique for programming authenticated data structures (ADSs) (an idea that this post will introduce). Our approach is implemented as a small extension to a general-purpose programming language. With this extension, we can establish security by typing: any type-correct program (which is a data structure implementation) implemented in our language will be secure. Thus we perform the proof once and for all, for all possible data structures, rather than having to prove security for each variation. Our approach exploits the compositional nature at the core of formal PL semantics and type systems to factor out the tedious part (the data structure logic) to focus on the security-relevant part (the use of cryptographic primitives). The proof ends up being pleasingly straightforward. The idea of security by typing is a powerful one that shows up frequently in PL-inspired work on security.
The remainder of this post — part 1 — introduces the idea of ADSs and why we want general-purpose support for them. The PL ideas show up in part 2, which will introduce our approach for building ADSs.
Filed under Secure computation
Securing computation
This post is the introduction of a series that discusses research bringing together ideas from the Programming Languages and Cryptography (Crypto) communities. The combination of ideas aims to produce secure computation technologies that are easier to use efficiently in a general-purpose setting, and easier to reason about, than when applying the Crypto ideas directly. My next post will be on work I’ve recently published in this area in collaboration with colleague cryptographers. Subsequent posts will consider other areas of interesting research (mostly not mine).
Filed under Secure computation