The PLUM reading group recently discussed the paper, DR CHECKER: A Soundy Analysis for Linux Kernel Drivers, which appeared at USENIX Securty’17. This paper presents an automatic program analysis (a static analysis) for Linux device drivers that aims to discover instances of a class of security-relevant bugs. The paper is insistent that a big reason for DR CHECKER’s success (it finds a number of new bugs, several which have been acknowledged to be true vulnerabilities) is that the analysis is soundy, as opposed to sound. Many of the reading group students wondered: What do these terms mean, and why might soundiness be better than soundness?
To answer this question, we need to step back and talk about various other terms also used to describe a static analysis, such as completeness, precision, recall, and more. These terms are not always used in a consistent way, and they can be confusing. The value of an analysis being sound, or complete, or soundy, is also debatable. This post presents my understanding of the definitions of these terms, and considers how they may (or may not) be useful for characterizing a static analysis. One interesting conclusion to draw from understanding the terms is that we need good benchmark suites for evaluating static analysis; my impression is that, as of now, there are few good options. Continue reading
This post presents an interview I did on March 10th, 2015, with Matt Might, a PL researcher who is an Associate Professor in the School of Computing at the University of Utah.
Matt has made strong scientific contributions to the field of programming languages, and he has done much more. He maintains an incredibly popular blog on wide-ranging topics (13 million pageviews since 2009 on topics from abstract interpretation to how to lose weight to how to be more productive). He has also become deeply committed to supporting people with rare diseases, including his own son, Bertrand, who was the first person diagnosed with NGLY1 deficiency. His work on rare disease propelled him to the White House: He met the President on January 31st, 2015, and he took a position in the Executive Office of the President to accelerate the implementation of the Precision Medicine Initiative on March 21st.
We had an engaging conversation covering all of these topics. It is too long for one post, so this post is the first of two. Continue reading
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.
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.
In this post, I introduce the emerging area of probabilistic programming, showing how probabilistic programs will hopefully make it easier to perform Bayesian-style machine learning, among other applications. Probabilistic programming is an exciting, and growing, area of research, with fantastic people in both AI/ML and PL working together and making big strides. PL methods — including formal semantics, optimization techniques, and forms of static analysis — have proven very useful in advancing this area forward.
[This is the second part of a two-post series. The first part is here.]
Recently, I talked about using program verifiers in teaching proof techniques in undergraduate CS, and my own experience with using the Dafny verifier in an algorithms class. One thing that that post was missing was a student perspective. So I asked three of my students — Julie Eisenberg, Rebecca Smith, and Matthew Dunn-Rankin — what they thought of Dafny. In this post, I summarize their insightful feedback and ponder about its implications.
The takeaway message for me is that verification tools such as Dafny are an excellent way of introducing students to formal proofs. At the same time, some care is needed as we integrate these tools with our pedagogy. In particular, the automated reasoning capabilities of Dafny aren’t an unadulterated blessing, and we must make sure that students understand how to do formal proofs fully manually. We ought to also invest more effort on tools that make the proof process more productive, for example by giving users more feedback on why an attempt at a formal proof failed. Continue reading
[This is the first part of a two-post series. The second part is here.]
In previous posts on this blog, I have talked about how research on programming languages and tools can contribute to K-16 education. In this post, I will share with you some of my experiences while trying to use a PL tool — specifically, a semi-automated program verifier — in an undergraduate algorithms class. The experience was a success in many ways. A program verifier gives students a hands-on understanding of how algorithms are mathematical objects, and verification tools are now mature enough for productive classroom use. I think every CS program would benefit students by introducing them to these tools at some point. At the same time, the experience exposed me to some serious limitations of current-day program verification, and opened up a number of directions for new research in this area. Continue reading
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
Automated analysis of programs is one of the major success stories in PL. The goal here is to algorithmically infer properties of a program’s runtime behavior without executing the program on concrete inputs. This may be done for many reasons, including optimization and reasoning about correctness. If you are trying to optimize a program, it helps to know that a statement executed within a loop always performs the same update, and can therefore be moved out of the loop. If you want to be certain that your C program doesn’t have buffer overflows, you want to infer bounds on the indices used for array accesses in the program.
Over the years, systems for program analysis have increased in sophistication and entered the mainstream of software development. But how do you know that what your analysis tells you is correct? To be certain that it is, we must relate the program’s semantics – what the program does at runtime – to what the analysis algorithm computes. The framework of abstract interpretation is the gold standard for doing so.
Radhia Cousot, co-inventor of abstract interpretation, passed away earlier this summer after a long struggle with cancer. While her death was tragic, I am consoled that she lived to see her work impact the world in a way that most researchers can only dream of.