From time to time, the PL Enthusiast will publish interviews of “new scientists on the block”: prominent PL researchers who are about to start, or just started, independent research careers in universities or research laboratories. This week, we feature Emina Torlak, who is starting as an assistant professor at the University of Washington in Fall 2014.
Monthly Archives: June 2014
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
Programming language research for K-16 education
At the recent PLDI conference, Armando Solar-Lezama and I organized a workshop called PLOOC: “Programming Language Tools for Massive Open Online Courses.” The high-level goal of the workshop was to discuss ways in which tools coming out of PL research can be used in K-16 education. Over the years, PL researchers have developed many techniques for automating and simplifying the design and analysis of programs. For the most part, these techniques have targeted the professional programmer. However, techniques developed for industrial code can also be applied to student-written programs in computer science courses.
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
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.
Filed under Abstract interpretation, Formal verification
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
Build-it, Break-it, Fix-it Programming Contest
Starting on August 28, Maryland is hosting an on-line, security-minded programming contest that we call Build-it, Break-it, Fix-it. If you are a graduate or undergraduate student at a US-based University, I encourage you to sign up – you could win significant prizes! Otherwise, please encourage students you know to participate.
The contest web site, with details about the event, is https://builditbreakit.org/
The subject of this blog post is a bit more about the contest, but primarily it is about our motivation for running it and what it has to do with programming languages. Continue reading
Filed under Software Security
Welcome to the PL Enthusiast!
Welcome to our blog about research and developments in programming languages (PL) and their applications and connections to areas across science and technology!
We are Michael Hicks and Swarat Chaudhuri, professors in computer science at the University of Maryland and Rice University, respectively, and we both have a great passion for programming languages.
More about our background and the goals and origins of this blog are explained on the About page.
We are now working on a series of posts across several threads:
- The role of PL in computer security
- Comparing PL theory and theory developed in the Algorithms community
- How PL can help us think about machine learning
- Highlights and tutorials on emerging programming languages
Stay tuned to this space; we look forward to your comments and contributions!
Filed under Uncategorized