Author Archives: Michael Hicks

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 | October 8, 2014 · 1:31 pm

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.

Continue reading →

2 Comments

Filed under Education, Software Security

Tagged as , ,

by | September 17, 2014 · 9:30 am

Advice on writing an author response

The POPL’15 author response period just ended a few days ago, and now submitted papers are in their final stages of review. Author response, a.k.a. author rebuttal, is a feature of conference review processes that allows authors to respond to claims made by reviewers prior to the final decision being made. The idea goes back at least as far as ISMM’06 in the PL community, but perhaps even further.

Following my previous post on advice for writing reviews, a commenter wondered whether I might also have advice for writing rebuttals. Indeed I do, and this post contains it. Your thoughts welcome!

Continue reading →

3 Comments

Filed under Process, Science

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 | August 21, 2014 · 8:30 am

Advice on reviewing papers

Recently I wrote a document for my students giving them advice on reviewing scientific papers, particularly those in programming languages. John Regehr recently blogged about reviewing papers efficiently (and Shriram Krishnamurthi before him), and it reminded me that I had this document, so I decided I would post it here, following up on my recent post on the importance of peer review. I hope that students and those interested in peer reviewing will find it useful.

The ideas in this post come from my experiences as a journal reviewer and editor, and as a program committee member and Chair. I outline how I believe that papers should be judged, and how to write a review to express that judgment. Judgments should involve usefulness/appeal, novelty, correctness, and exposition. Reviews should aim to be self-contained, clearly expressing support for their recommendation; constructive, providing feedback for improving the work; and respectful of the authors who put a lot of time into their research. In general, think of the kind of review you’d like to receive, and act accordingly.

Continue reading →

5 Comments

Filed under Process, Science

by | August 18, 2014 · 8:06 am

Remembering Professor Susan B. Horwitz

[Guest poster Thomas Ball of Microsoft Research remembers his Ph.D. advisor, Professor and programming languages researcher Susan Horwitz, who recently passed away. –Mike]

Continue reading →

3 Comments

Filed under Program Analysis, Scientists

Tagged as , , ,

by | August 14, 2014 · 8:53 am

Peer review, and why it matters

Scientific results intersect with all aspects of the modern world, and they underpin many important decisions made at the level of governments, corporations, and individuals. When you read about a scientific result—like the correlation of a particular gene’s mutation with a certain disease, or that it’s better for children to engage in unstructured play rather than structured learning at early ages—why should you believe it?

If you were an expert, you might be able to (with time) capably judge the work itself. But what if you are a non-expert, which is increasingly likely as branches of study become hyper-specialized? In this case, you are left to trust the scientific process, i.e., the way in which scientific work is judged to be true and important. At the heart of this process is peer review.

In this post I describe elements of the peer review process we use in scientific research about programming languages.

Continue reading →

19 Comments

Filed under Process, Science

by | August 5, 2014 · 7:15 am

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.

Continue reading →

40 Comments

Filed under Dynamic languages, PL in practice, Semantics, Software Security, Types

by | July 21, 2014 · 7:09 am

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!

Continue reading →

69 Comments

Filed under PL in practice, Semantics, Software Security

Tagged as , , , ,

by | July 10, 2014 · 7:30 pm

IEEE posts its top list of languages

In a funny coincidence following my last post on language adoption, the IEEE Spectrum in my mailbox today contained a pointer to IEEE’s version of the top N languages.

They use a variety of data sources, some of which overlap with the SocioPLT’s, e.g., counting projects on GitHub. Some sources are different, e.g., using Google and Twitter to count occurrences of “X programming” for a language X. The site allows you to create your own rankings to weigh the various data sources differently, e.g., to focus only on GitHub projects or to increase the weight of Google Trends.

Comparing the IEEE top twenty with the SocioPLT top twenty shows some interesting differences.

Continue reading →

6 Comments

Filed under Uncategorized