Category Archives: Formal verification

by | February 4, 2019 · 1:00 pm

“What is PL Research?” The Talk

I was invited to give a talk at the Programming Languages Mentoring Workshop (PLMW) colocated with POPL’19 in January. The talk topic was What is programming languages research? I was excited to give this talk. It’s a topic I’ve thought a lot about over the years; in 2015 I wrote a blog post about it. Shortly thereafter I was elected SIGPLAN Chair, and over the ensuing three years came to know the exciting depth and breadth of the field even more deeply.

Like the blog post, the talk presents what I view as the goals, ethos, and benefits of PL research. Because the PLMW audience is senior undergraduates and early graduate students, the talk also presents an overview of PL as a field. In particular, it presents a tutorial of sorts of the areas and methods that PL researchers often develop and employ. To capture what these are, I skimmed a sampling of the conference proceedings of PLDI and POPL from the last 30 years. Doing so, I abstracted the “shape” of a PL research paper, and identified the broad areas PL researchers tend to focus on. The talk presents a flavor of these areas. Because the talk took place just before POPL, I focused most on topics that appear in POPL-published research; the talk highlights particular POPL’19 papers as examples.

Several people afterward told me that they enjoyed the talk and asked about whether a video of the talk might be available. Unfortunately, the talks were not recorded. SIGPLAN main conference talks are regularly video-recorded, but workshops and co-located events are hit and miss. I certainly understand the financial reasons for this situation. Nevertheless, it’s really too bad that PLMW talks are not recorded. In my experience, PLMW speakers put an exceptional amount of time and care into their talks, so they are often very well done. The talks also target a general audience, so they are potentially valuable to many more people than just those attending the actual event.

In the hopes that others might find it useful, I decided to video-record myself giving the PLMW talk. The recording is not great, but I hope that fact doesn’t get in the way of the conveying the content. If it does, maybe just the slide deck will prove useful. If you have comments or thoughts, I’m glad to hear them!

Many thanks to the organizers of PLMW@POPL’19 for a great event, and the opportunity to speak!

The video. The slides.

12 Comments

Filed under Abstract interpretation, Process, Program Analysis, Research, Semantics, Types

Tagged as

by | October 23, 2017 · 1:00 pm

What is soundness (in static analysis)?

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 →

35 Comments

Filed under Abstract interpretation, Program Analysis

Tagged as , , , ,

by | March 24, 2016 · 1:00 pm

Interview with Matt Might

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 Might headshot

Matt Might

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 →

3 Comments

Filed under Abstract interpretation, Bioinformatics, Dynamic languages, Interviews, Program Analysis, Science, Scientists

Tagged as , , ,

by | December 23, 2014 · 2:21 pm

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.

Continue reading →

1 Comment

Filed under Formal verification, Program Analysis, Secure computation, Semantics, Software Security, Uncategorized

Tagged as , , , , , , , , , ,

by | December 17, 2014 · 2:00 pm

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.

Continue reading →

3 Comments

Filed under Formal verification, Research, Research directions, Secure computation, Software Security

Tagged as , , , , , ,

by | September 8, 2014 · 10:58 am

What is probabilistic programming?

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.

Continue reading →

11 Comments

Filed under Formal verification, Probabilistic programming, Program Analysis, Semantics

Tagged as , ,

by | July 28, 2014 · 3:32 pm

Program verification in the undergraduate CS curriculum (Part II)

[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 →

1 Comment

Filed under Education, Formal verification, MOOCs

by | July 17, 2014 · 9:23 am

Program verification in the undergraduate CS curriculum

[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 →

5 Comments

Filed under Education, Formal verification

by | July 1, 2014 · 10:56 am

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 →

14 Comments

Filed under Formal verification, Software Security

by | June 9, 2014 · 4:19 am

Radhia Cousot

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.

Continue reading →

3 Comments

Filed under Abstract interpretation, Formal verification

Tagged as , ,