Five Research Ideas Instagram Could Have Used to Protect Comey's Secret Twitter

Even though cybersecurity is one of the hottest topics on the Internet, my specific area of research, information flow security, has remained relatively obscure. Until now, that is.

You may have heard of "information flow" as a term that has been thrown around with terms like "data breach," "information leak," and "1337 hax0r." You may not be aware that information flow is a specific term, referring to the practice of tracking sensitive data as it flows through a program. While techniques like access control and encryption protect individual pieces of data (for instance, as they leave a database), information flow techniques additionally protect the results of any computations on sensitive data.

Information flow bugs are usually not the kinds of glamorous bugs that make headlines. Many of the data leaks that have been in the public consciousness, for instance the Target and Sony hacks, happened because the data was not protected properly at all. In these cases, having the appropriate access checks, or encrypting the data, should do the trick. But "why we need to protect data more better" is harder to explain. Up through my PhD thesis defense, I had such a difficult time finding headlines that were actually information flow bugs that I resorted to general software security motivations (cars! skateboards! rifles!) instead.

From the article.

Then along came "This Is Almost Certainly James Comey's Twitter Account," an article I have been waiting for since I started working on information flow in 2010. The basic idea behind the article is this: a journalist named Ashley Feinberg wanted to find FBI director James Comey's secret Twitter account, and so started digging around the Internet. Feinberg was able to be successful within four hours due to being clever and a key information leak in Instagram: when you request to follow an Instagram account, it makes algorithmic suggestions based on who to follow. And in the case of this article, the algorithmic suggestions for Comey's son Brien included several family members, including James Comey's wife--and the account that Feinberg deduced to be James Comey's. And it seems that Comey uses the same "anonymous" handle on Instagram as he does on Twitter. And so Instagram's failure to protect Brien Comey's protected "following" list led to the discovery of James Comey's Twitter account.

So what happened here? Instagram promises to protect secret accounts, which it (sometimes*) does. When one directly views the Instagram page of a protected user, they cannot access that person's photos, who that user is following, and who follows that user. This might lead a person to think that all of this information is protected all of the time. Wrong! It turns out the protected account information is visible to algorithms that suggest other users to follow, a feature that becomes--incorrectly--visible to all viewers once a follow is requested, because, presumably, whoever implemented this functionality forgot an access check. In this case the leak is particularly insidious because while the profile photos and names of the users shown are all already public, they are likely shown as a result of a computations on secret information: Brien Comey's protected follow information. (This is a subtle case to remember to check!) In information flow nomenclature, this is called an implicit flow. When someone is involved in a lot of Instagram activity, the implicit flow of the follow information may not be so apparent. But when many of the recommended follows are Comey family members, many of them who use their actual names, this leak becomes more serious!

Creepy Facebook search, from express.co.uk.

In the world of information flow, this article is a Big Deal because it so perfectly illustrates why information flow analyses are useful. For years, I had been jumping up and down and waving my arms (see here and here, for instance) about why we need to check data in more places than the point where it leaves the database. Applications aren't just showing sensitive values directly anymore, but the results of all kinds of computations on those values! (In this case it was a recommendations algorithm.) We don't always know where sensitive data is eventually going! (As was the case when Brien Comey's protected "following" list was handed over to the algorithm.) Policies might depend on sensitive data! We may even compute where sensitive data is going based on other sensitive data! In a world where we can search over anything, no data is safe!

Until recently, my explanations have seemed subtle and abstract to most, in direct contrast to the sexy flashy security work that people imagine after watching Hackers or reading Crypto. By now, though, we information flow researchers should have your attention. We have all kinds of computations over all kinds of data going to all kinds of people, and nobody has any clue what is going on in the code. Even though digital security should be one of the main concerns of the FBI, Comey is not able to avoid the problems that arise from the mess of policy spaghetti that is modern code.

Fortunately, information flow researchers have been working for years on preventing precisely this kind of Comey leak**. In fashionable BuzzFeed style, I will list exactly five research ideas Instagram could adapt to prevent such leaks in the future:

1. Static label-based type-checking. In most programming languages, program values have types. Type usually tell you simple things like whether something is a number or a list, but they can be arbitrarily fancy. Types may be checked at compile time, before the program runs, or at run time, while the program is running. There has been a line of work on static (compile time) label-based information flow type systems (starting with Jif for Java, with a survey paper here describing more of this work) that allows programmers to label data values with security levels (for instance, secret or not) as types, and that propagate the type of a program that makes sure sensitive information does not flow places that are less sensitive. These type systems give guarantees about any program that runs. The beauty of these type systems is that while they look simple, they are clever enough to be able to capture the kind of implicit flow that we saw with algorithms leaking Brien Comey's follow information. (We'd label the follow lists as sensitive, and then any values computed from them couldn't be leaked!)
2. Static verification. Label-based type-checking is a light-weight way of proving the correctness of programs according to some logical specification. There are also heavier-weight ways of doing it, using systems that translate programs automatically into logical representations, and check them against the specification. Various directions of work using refinement types, super fancy types that depend on program values could be used for information flow. An example of a refinement type is {int x | canSee(alice, x)}, the type of a value that exists as an integer x that can only exist if user "alice" is allowed to see it according to the "canSee" function/predicate) Researchers have also demonstrated ways of proving information flow properties in systems like IronClad and mKertiKOS. These efforts are pretty hardcore and require a lot of programmer effort, but they allow people to prove all sorts of boutique guarantees on boutique systems (as opposed to the generic type system guarantees using the subset of a language that is supported).
3. Label-based dynamic information flow tracking. Static label-based type-checking, while useful, often requires the programmer to put labels all over programs. Systems such as HiStar, Flume (the specific motivation of which was the OKCupid web server), and Hails allow labeling of data in a way similar to static label-based type systems, but track the flow of information dynamically, while the program is running. The run-time tracking, while it makes it so that programmers don't have to put labels everywhere, comes at a cost. First, it introduces performance slowdowns. Second, we can't know if a program is going to give us some kind of "access denied" error before it runs, so there could be accesses denied all over the place. Many of these systems handle these problems by doing things at the process level: if there is an unintended leak anywhere in the process, the whole process aborts. (Those who haven't heard of processes can think of the process as encapsulating a whole big task, rather than an individual action, like doing a single arithmetic operation.)
4. Secure multi-execution. Secure multi-execution is a nice trick for running black-box code (code that you don't want to--or can't--change) in a way that is secure with respect to information flow. The trick is this: every time you reach a sensitive value, you execute the sensitive value in one process, and you spawn another process using a secure default input. The process separation guarantees that sensitive values won't leak into the process containing the default value, so you know you should always be allowed to show the result of that one. As you might guess, secure multi-execution can slow down the program quite a bit, as it needs to spawn a new process every time it sees a sensitive value. To mitigate this, my collaborators Tom Austin and Cormac Flanagan developed a faceted execution semantics for programs that lets you execute a program on multiple values at the same time, with all of the security guarantees of secure multi-execution.
5. Policy-agnostic programming. While all of these other approaches can prevent sensitive values from leaking information, if we want programs to run most of the time, somebody needs to make sure that programs are written not to leak information in the first place. It turns out this is pretty difficult, so I have been working on programming model that factors information flow policies out of the rest of the program. (If I'm going to write a whole essay about information flow, of course I'm going to write about my own research too!) Instead of having to implement information flow policies as checks across the program, where any missing check can lead to a bug, type error, or runtime "access denied," programmers can now specify each policy once, associated with the data, along with a default value, and rely on the language runtime and/or compiler to make the code execute according to the policies. In the policy-agnostic system, the programmer can say that Brien Comey's follows should only be visible to followers, and the machine becomes responsible for making sure this policy is enforced everywhere, including the code implementing the recommendations algorithm. That policies can depend on sensitive values, that sensitive values may be shown to viewers whose identities are computed from sensitive values, and that enforcing policies usually implementing access checks across the code are all challenges. Our semantics for the Jeeves programming language (paper here) addresses all of these issues using a dynamic faceted execution approach, and we have also extended this programming model to handle applications with a SQL database backend (paper here). We are also working on a static type-driven repair approach (draft here).

I don't know how much this Twitter account leak upset the Comeys, but reading this article was pretty much the most exciting thing that I have ever done. Up until now, most people have thought about security in terms of protecting individual data items, rather than in terms of a complex and subtle interaction with the programs that use them. This has started to change in the last few years as people have been realizing just how much of our data is online, and just how unreliable the code is that we trust with this data. I hope that this Comey leak will cause even more people to realize how important it is to reason deeply about what our software is doing. (And to fund and use our research. :))

* A student in my spring software security course (basically, programming languages applied to security), Scott, had noticed earlier this semester that emails from Instagram allowed previews of protected accounts he was not following. He reported this to Facebook's bug bounty program and made $1000. I told him to please write in the course reviews that the course helped him make money.
** Note that a lot of other things are going on in this Comey story. The reporter used facts about Comey to figure out the setup, and also some clever inference. But this clever inference exploited a specific information leak from the secret follows list to the recommendations list, and this post focuses on this kind of leak.

Counter-Advice for the PhD

Recently I attended the Programming Languages Mentoring Workshop, a program to introduce advanced undergraduates and early-stage PhD students to research in general and research in our field. (By the way, this is a fantastic workshop and I highly encourage students to attend!) While listening to advice from other academics and talking to the students about their questions, I realized that I have come to disagree with much of the conventional wisdom and advice for PhD students, some of which I have been guilty of re-dispensing. I express my dissent here.

Clarification: The workshop was not the source of all of the quotes! It was simply what got me thinking about the dangers of taking any one piece of advice too seriously. (The workshop itself is great for showcasing different points of view.)

--

"To decide what to work on, read lots of papers and then choose the best problem."
One of my undergraduate professors once told me, "Take all advice with a grain of salt. Most advice is highlights and wishful thinking." This was one of the best pieces of advice anyone has ever given me. It is easy for people to give this kind of advice about choosing research problems after they have learned what makes a good research problem. The advice is far more difficult to follow for people who are still developing their research taste. While some people probably have chosen research problems this way and while it is helpful to more deeply understand your area, early-stage researchers sometimes just have to jump in, do things, and learn from the confusion.

Also, in the early stages of a PhD, developing research skills (project management, time management, and communication of results) can be far more important than working on the best problem. In this case, I would recommend working on a problem that a mentor is sufficiently invested in to help you gain the skills you need.

--

"Choose an advisor you are completely compatible with."
This advice goes in the same category as the previous one. Once you have gone through the PhD and developed a deep understanding of who you are and who your advisor is, it is easy to think that a good situation can be easily recreated or a bad situation could have been more easily avoided. While you should look enough into your soul and do enough due diligence to make sure there are no glaring red flags, you should not worry if you do not feel like you know enough about your working style or preferences to choose a perfectly compatible advisor. Advisor-advisee relationships, like all other human relationships, depend a lot on many factors, only some of which are under the control of the two main participants, and also can evolve quite a bit over time.

--

"Do a PhD because you are in love."
 I completely agree that doing a PhD out of love of learning, love of discovery, or love for a discipline is a much better reason than doing a PhD for the money, fame, or glory. But I've seen many students get stuck in the "passion trap," the idea that you need to be completely in love with something before you invest significant amounts of time and energy into it. According to Cal Newport, who has written extensively about this, passion is something that often comes later, after you have become an expert and people recognize you for your contributions.

What I have noticed is that people often differ more in the narratives they have about their relationships with their work than in their actual relationships with their work. In my Quora answer to the question "How common is it for PhD students to do work they are not passionate in?" I talk about how one's relationship with a project often follows a trajectory similar to a romantic relationship: infatuation, followed by a steady state that comes sometime later, often much later, with a period of confusion and negotiation in between. I've seen every researcher I know well experience the confusion phase, but some researchers are more open than others to talking about it.

A side observation is that relationships with research seem to vary culturally: for instance, being blanket positive about one's own research seems to go along with the American tendency to be blanket positive about one's own life.

--

"Superstars are born, not made."
No one has said this specific phrase to me, but many people have implied it with the qualities they value in students. Once a professor told me that some students "just can't cut it." I've seen professors pick favorites based on internal metrics they have (often, it seems, based on how much a student reminds them of themselves). I've seen students decide someone is the smartest among them because of confidence, or some other "star" quality that doesn't necessarily correlate directly with research skill. While there is a baseline level of intelligence, curiosity, drive, and tolerance for uncertainty that someone needs to be a good researcher, many of the qualities that make a great researcher--discipline and persistence, to name two--are not entirely innate and definitely not strongly correlated with the confidence and charisma that seem to build many star reputations. (Note: confidence and charisma can also be learned.)

--

"The PhD is lonely without a significant other, especially if you are a woman in a male-dominated field."
I was surprised that people have told me this--and that, at least when I was starting my PhD, there was a common conception that having a romantic partner was somehow necessary for enduring the trials of the PhD. While it is important to nurture healthy relationships with supportive people, a significant other does not need to be one of them. Especially in relationships between people of similar levels of ambition, it can become tricky to negotiate coevolution and colocation, thus adding unnecessary pressure to the PhD experience. (And, unfortunately, because of society's insistence on holding on to gender roles, women who date men often find themselves with more pressure to conform to their partner's desires.) During my PhD, I had many friends, some of them women in male-dominated fields, many who ended up becoming stars in their fields, who were happily single for significant portions of their PhD.

--

"The most successful PhD students work all the time."
See my answer (and other answers) to the Quora question "Do Ph.D. students have time for hobbies?" Nurturing a relationship with a significant other also counts as a hobby, so you can do that too if that's what you want.

--

"If it's not hard, it's not worth doing."
There is something to be said for only doing things that help you grow in some way, but there is necessary challenge and then there is unnecessary challenge. During the PhD, it is necessary to come to terms with uncertainty, confusion, and possible rejection of your ideas from the community. This is crucial for one's development into a full-fledged researcher. What is less necessary, however, is depriving yourself of food or sleep, always working to the point of exhaustion, or mismanaging your time so that you are always under deadline pressure. For some people it may be necessary to endure toxic advisor or collaborator relationships, but I would encourage those people to seek ways out of that if possible--abuse does not need to go hand-in-hand with growth. Self-inflicted struggle only makes the necessary struggle more difficult.

--

I hope you realize by now that there is no single right way to do the PhD and that there are many valid--and sometimes conflicting--views on what a good path is. Have fun with the confusion. :)

Why It's Not Academia's Job to Produce Code That Ships

Note: The images in this post are inexplicably broken due to some kind of Blogger bug. If someone is reading this at Google, please help!

My scientist friends often scoff at crime show writers' creative interpretation of technology's limits.

The technology shiny world of CSI: Cyber.

"Let's zoom in here," a character says in an investigation room with floor-to-ceiling screens showing high-definition maps of the show's major metropolitan area. A flick of the fingers reveals an image of the suspect at mouth-watering resolution.

In another scene, the characters listen to a voice mail from the suspect. "What's that in the background?" one investigator asks. Using an interface that deadmau5 would kill to have, the hacker of the bunch strips out the the talking, the other sounds. They say some words like "triangulation" and, eureka, they deduce the suspect's exact location.

Yes, real police technology is nowhere near this sophisticated. Yes, nobody (except maybe the government, secretly) has technology like this. But those who criticize the lack of realism are missing the point.

The realities that art constructs take us out of our existing frames of perception--not only for fun, but also for profit. Many important technological advances, from the submarine from the cell phone, appeared in fiction well before they appeared in real life. Correlation does not imply causation, but many dare say that fiction inspires science.

Some complaints against academic Computer Science.

This brings us to the relationship between academic Computer Science and the tech industry. Recently, people in industry have made similar criticisms of academic computer science. Mike Hoye of Mozilla started the conversation by saying he was "extremely angry" with academics for making it difficult for industry to access the research results. This unleashed a stream of Internet frustration against academics about everything from lack of Open Access (not our faults) to squandering government funding (not entirely true) to not caring about reproducibility or sharing our code (addressed in an earlier blog post).

At the heart of the frustration is a legitimate accusation*: that academics care more about producing papers than about producing anything immediately (or close to immediately) useful for the real world. I have been hearing some variation of this criticism, from academics as well as industry people, for longer than I have been doing research. But these criticisms are equivalent to saying that TV writers care more about making a good show than being technically realistic. While both are correct observations, they should not be complaints. The real problem here is not that academics don't care about relevance or that industry does not care about principles, but that there is a mismatch in expectations.

It makes sense that people expect academic research results to work in companies right away. Research that makes tangible, measurable contributions is often what ends up being most popular with funding sources (including industry), media outlets, and other academics reviewing papers, faculty applications, and promotion cases. As a result, academic researchers are increasingly under pressure to do research that can be described as "realistic" and "practical," to explicitly make connections between academic work and the real, practical work that goes on in industry.

In reality, most research--and much of the research worth doing--is far from being immediately practical. For very applied research, the connections are natural and the claims of practicality may be a summer internship or startup away from being true. Everything else is a career bet. Academics bet years, sometimes the entirety, of their careers on visions of what the world will be like in five, ten, twenty years. Many, many academics spend many years doing what others consider "irrelevant," "crazy," or "impossible" so that the ideas are ready by the time the time the other factors--physical hardware, society--are in place.

The paths to becoming billion-dollar industries.

In Computer Science, it is especially easy to forget that longer-term research is important when we can already do so much with existing ideas. But even if we look at what ends up making  money, evidence shows that career bets are responsible for much of the technology we have today. The book Innovation in Information Technology talks about how ideas in computer science turned into billion-dollar ideas. A graphic from the book (on right) shows that the Internet started as a university project in the sixties. Another graphic shows there were similarly long tech transfer trajectories for ideas such as relational databases, the World Wide Web, speech recognition, and broadband in the last mile.

The story of slow transfer is true across Computer Science. People often ask me why I do research in programming languages if most of the mainstream programming languages were created by regular programmers. It we look closely, however, most of the features in mainstream languages came out of decades of research. Yes, Guido Van Rossum was a programmer and not a researcher before he became the Benevolent Dictator of Python. But Python's contribution is not in innovating in terms of any particular paradigm, but in combining well features like object orientation (Smalltalk, 1972, and Clu, 1975), anonymous lambda functions (the lambda calculus, 1937), and garbage collection (1959) with an interactive feel (1960s). As programming languages researchers, we're looking at what's next: how to address problems now that people without formal training are programming, now that we have all these security and privacy concerns. In a media interview about my Jeeves language for automatically enforcing security and privacy policies, I explained the purpose of creating research languages as follows: "We’re taking a crazy idea, showing that it can work at all, and then fleshing it out so that it can work in the real world."

Some may believe that all of the deep, difficult work has already been done in Computer Science--and now we should simply capitalize on the efforts of researchers past. History has shown that progress has always gone beyond people's imaginations. Henry Leavitt Ellsworth, the first Commissioner of the US Patent Office, is known to have made fun of the notion that progress is ending, saying, "The advancement of the arts, from year to year, taxes our credulity and seems to presage the arrival of that period when human improvement must end." And common sense tell us otherwise. All of our data is becoming digitized and we have no clue how to make sure we're not leaking too much information. We're using software to design drugs and diagnose illness without really understanding what the software is doing. To say we have finished making progress is to be satisfied with an unsatisfying status quo.

The challenge, then, is not to get academics to be more relevant, but to preserve the separate roles of industry and academia while promoting transfer of ideas. As academics, we can do better in communicating the expectations of academic research (an outreach problem) and developing more concrete standards of expectations for "practical" research (something that Artifact Evaluation Committees have been doing, but that could benefit from more input from industry). As a society, we also need to work towards having more patience with the pace of research--and with scientists taking career bets that don't pay off. Part of the onus is on scientists for better communicating the actual implications of the work. But everyone else also has a responsibility to understand that if we're in the business of developing tools for an unpredictable future--as academics are--it is unreasonable to expect that we can fill in all the details right away, or that we're always right.

It is exciting that we live in a time when it is possible to see technical ideas go from abstract formulations to billion-dollar industries in the course of a single lifetime. It is clear we need to rethink how academia and industry should coexist under these new circumstances. Asking academics to conform to the standards of industry, however, is like asking TV writers to conform to the standards of scientists--unnecessary and stifling to creativity. I invite you to think with me about how we can do better.

With thanks to Rob Miller and Emery Berger for helping with references.

* Note that this post does not address @mhoye's main complaint about reproducibility, for which the response is that, at least in Programming Languages and Software Engineering, we recognize this can be a problem (though not as big of a problem as some may think) and have been working on it through the formation of Artifact Evaluation Committees. This post addresses the more general "what are academics even doing?!" frustration that arose from the thread.

--

Addendum: Many have pointed out that @mhoye was mainly asking for researchers to share their code. I address the specific accusation about academics not sharing code in a previous blog post. I should add that I'm all for sharing of usable code, when that's relevant to the work. In fact, I'm co-chairing the POPL 2017 Artifact Evaluation Committee for this reason. I'm also all for bridging the gaps between academia and industry. This is why I started the Cybersecurity Factory accelerator for turning commercializing security research.

What I'm responding to in this post is the deeper underlying sentiment responsible for the misperception that academics do not share their code, the sentiment that academics are not relevant. This relevance, translating roughly into "something that can be turned into a commercial idea" or "something that can be implemented in a production platform" is what I mean by "shipping code." For those who wonder if people really expect this, the answer is yes. I've been asked everything from "why work on something if it's not usable in industry in the next five years?" to "why work on something if you're not solving the problems industry has right now?"

What I'd like is for people to recognize that in order for us to take bets on the future, not all research is going to seem relevant right away--and some if might never be relevant. It's a sad state of affairs when would-be Nobel laureatees end up driving car dealership shuttles because they failed to demonstrate immediate relevance. Supporting basic science in computer science involves patience with research.

Myth: "CS Researchers Don't Publish Code or Data"

A collaboration with Sam Tobin-Hochstadt, Assistant Professor at Indiana University.

There has been some buzz on social media about this "Extremely Angry" Twitter thread. Mike Hoye, Engineering Community Manager for Firefox at Mozilla expressed frustration about getting access to the products of research. It turns out that many other people are angry about this too.

While there are certainly legitimate aspects to these complaints, we’d like to address a specific misperception from this Twitter thread: the claim that "CS researchers don't publish code or data." The data simply shows this is not true.

First of all, while the Repeatability in Computer Science study from a few years ago highlighted some issues with reproducibility in our field, it revealed that a significant fraction of researchers (226 out of 402) in systems conferences have code available either directly linked from the paper, or on request.

Additionally, in the last few years, conferences in Programming Languages and Software Engineering have been pushing for more standardization of code-sharing and repeatability of results through Artifact Evaluation Committees. There is a comprehensive summary of Artifact Evaluation in our field here. (In fact, Jean is co-chairing the POPL 2017 AEC with Stephen Chong.) According to the site, artifacts are evaluated according to the following criteria:

• Consistent with the paper. Does the artifact substantiate and help to reproduce the claims in the paper?
• Complete. What is the fraction of the results that can be reproduced?
• Well documented. Does the artifact describe and demonstrate how to apply the presented method to a new input?
• Easy to reuse. How easy is it to reuse the provided artifact? 

The most detailed documentation is associated with the AEC for OOPSLA 2013, where 50 papers were accepted, 18 artifacts passed evaluation, and 3 artifacts were rejected. For PLDI 2014, 20 of of 50 papers submitted artifacts and 12 passed. By PLDI 2015, 27 papers (out of 52) had had approved artifacts. Even POPL, the “theoretical” PL conference, had 21 papers with approved artifacts by 2016.

For those wondering why more artifacts are not passing yet, here is a transcribed discussion by Edward Yang from PLDI 2014. The biggest takeaways are that 1) many people care about getting the community to share reproducible and reusable code and 2) it takes time to figure out the best ways to share research code. (That academia’s job is not to produce shippable products, as Sam pointed out on Twitter, is the subject of a longer conversation.)

While it’s going to take time for us to develop practices and standards that encourage reproducibility and reusability, we’ve already seen some improvements. Over the years, Artifact Evaluation has become more standardized and committees have moved towards asking researchers to package code in VMs if possible to ensure long-term reproducibility. Here are the latest instructions for authors.

Yes, we can always do better to push towards making all of our papers and code available and reusable. Yes, researchers can do better in helping bridge the communication gap between academia and industry--and this is something we've both worked at. But the evidence shows that the academic community is certainly sharing our code--and that we’ve been doing a better job of it each year.

Note: It would be really cool if someone did a survey of individual researchers. As Sam pointed out on Twitter, many of our colleagues use GitHub or other social version control and push their code even before the papers come out.

--

UPDATE! Here is a survey for academics to report on how we share code. Please fill it out so we can see what the numbers are like! Thanks to Emery Berger, Professor at UMass Amherst, for conducting the survey.

Related update. Some conversations with others reminded me that the times I haven't shared my code, it has been because I was collaborating with companies and corporate IP policies prevented me from sharing. (In fact, this was one of the reasons I preferred to stay in academia.) The survey above asks about this. I'm curious how the numbers come out.

Experiment: Daily GitHub Checkins

I've been doing a lot of relatively mindless but decently labor-intensive code-related work (colloquially known, especially in the brogrammer community, as "coding bitch work"). I've been building up some web-based case studies in my Jeeves programming language. I've also had to take over some student code. Taking over this code was particularly painful because of all the managerial regret I felt: regret about not having made them document better, about not having made them do more work. The takeover process has involved a lot of commenting, test-writing, and the occasional small extension to test that I really know What's Going On.

Anyway, to try to mitigate the pain of these various tasks, or to spread it out and prolong it, I've decided to break from my usual model of nothing-nothing-nothing-OMGdeadline and do a small task every day that I work (which, note, does not include all days), big enough to warrant a GitHub checkin. (For those on the outside, being a computer science PhD student, at least if you're me, involves a lot of paper-reading, talk-preparing, writing, thinking, and "thinking" in addition to coding.) I hypothesized that this would be good for me to make incremental progress on some things that just aren't fun to do, as well as improve the general documentation state and cleanliness of my code and tools. I get pretty obsessed with arbitrary routine, so it's worked out decently well so far. (Check me out.) This policy has definitely made me write some documentation and tests I otherwise would not have written. (Although my pseudo-officemate Joe would argue that this is not "real work.") I'll report on things after we hit "OMGdeadline" and let you know how well it worked.

In the spirit of doing things in smaller increments, I'm also making it a goal to do smaller blog posts instead of the Blog Essays (also see my profile on Medium) I've gotten into a habit of doing. I've dramatically curbed my email habit (I wrote a thing here), so maybe these more frequent blog checkins will give my pent-up words somewhere to go.

Treat Yo Self: Clean Up Your Code

A couple years ago, I discovered what I thought was the shortcut to building research systems.  Forget good software engineering practice!  Forget functional abstraction!  Copy-and-paste code all over the place; modify it to fit your needs.  Thinking before coding?  So college.  After all, premature optimization is the root of all evil.

In the beginning, this worked out well.  In my first year, even my advisor told me he was impressed with how quickly I got things working.  I saw in other research code the same patterns that I was learning to adopt: monstrous tangles of functionality with scant documentation.  I have found the secret to research productivity, I thought.

A couple deadlines later, I began to feel the consequences of my actions.  Pre-deadline, systems would begin to fall apart: a patch here revealed another hole there.  Post-deadline I had no desire to go back to disgusting soups of one-off functions, barely usable in the first place and certainly not reusable.  Much time was spent either avoiding my code or writing replacement code from scratch.

In other researchers, I observed that the few who had designed their systems well were able to make quick bug fixes and extensions.  For everyone else, either their code bit-rotted in obscurity or they were a slave to maintaining their systems for barely-satisfied users.  During paper deadlines, those who had built up good infrastructure could build comfortably on previous work while others ran around fighting fires and despairing.

During the course of grad school, my relationship with my code has become increasingly important.  Clean, modular, and well-documented code (with tests!) is not only less likely to have bugs but will be useful for longer.  Clean code provides a solid foundation for you and potentially other researchers.  Modular code makes it easier to reuse parts of your code. Also, knowing exactly what your code does just feels good.

On his blog, Harvard professor Michael Mitzenmacher advises graduate students to take a day every now and then to find better tools: for organizing papers read, for recording ideas and progress, etc.  Rewriting and refactoring code has become an important part of these activities for me.  Not only is refactoring useful, but it is also a relatively low-effort way to achieve a feeling of progress*.  For me, refactoring has become a treat for working hard.

Don't tell too many people now, but I think this is the real secret to research productivity.

* The importance of the feeling of progress is a topic worthy of its own blog post.

Verve as a CACM Research Highlight

My paper with Chris Hawblitzel "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System" appeared as a Research Highlight (read here) of the Communications of the Association of Computing Machinery (CACM) in December. This is a shortened version of our 2010 paper appearing at the Programming Language Design and Implementation (PLDI) conference altered for a more general audience.

This paper describes the Verve operating system, the first operating system verified end-to-end and automatically for type safety. This means that programs running in Verve cannot suffer from whole classes of memory-related errors. The main idea of Verve is to implement the operating system in a type-safe language (C#), write a specification for the memory interface between the type-safe parts and the lower-level parts (the C# code does not mess up the stack; the low-level code does not mess up the heap), and verify the low-level parts of the system (in our case, using Boogie that translates to x86 assembly).

An exciting thing is that Xavier Leroy, who is responsible for both OCaml and the CompCert verified C compiler, wrote the Technical Perspective, "Safety First!" He writes, "The formal verification of high-assurance software is making great progress lately. Yang and Hawblitzel's work, along with other recent breakthroughs in software verification such as the seL4 verified microkernel of Klein et al. (see Communications, June 2010, p. 107), were unthinkable 10 years ago. Little by little, one point at a time, these results sketch a promised land where, with mathematical certainty, software does behave properly after all."

Another exciting thing for current graduate students interested in this work is that my Microsoft Research mentor Chris Hawblitzel is looking for a summer intern to work on adding concurrency to Verve. Not only was Chris Hawblitzel amazing for helping me learn everything I needed for this project, but he was also a fun mentor. I recommend that you contact him ASAP if you are interested in working with his this summer.

Research Update: A Language for Automatically Enforcing Privacy Policies

For the last three years, I have been working on things building up to the creation of Jeeves (project website here), a new programming language for automatically enforcing privacy policies. Last week I presented our first paper on Jeeves at the Principles of Programming Language (POPL) conference. You may read our paper here and look over the slides here.

To describe Jeeves I will quote Jacob Aron, who does a good job in this recent New Scientist article:

Even with your friends under control, a software bug could still expose your private data - as Facebook CEO Mark Zuckerberg himself found out recently when a glitch revealed his photos to the world. To solve this, researchers at the Massachusetts Institute of Technology have come up with a new programming language called Jeeves that automatically enforces privacy policies.

Programmers have to explicitly ensure data flowing through their software obeys necessary privacy policies, but it is easy to slip up and let information leak out. Jeeves solves that by substituting the value of variables within the software depending on who the user is. For example, say Alice posts a message but doesn't want anyone but herself to see who wrote it. The programmer can use the variable "author" without worrying what the user sees - when the software runs, Jeeves ensures Alice will see her own name, but everyone else logging in will see "Anonymous".

Jean Yang, who helped develop Jeeves, says the new language lets a programmer delegate privacy responsibilities and concentrate on the actual function of their code, much like a party host might entrust their butler with ensuring the needs of each guest are met so they can spend more time socialising.

Jeeves allows the programmer to provide high-level declarative policies for privacy and rely on the runtime system to automatically produce outputs adhering to these policies. The Jeeves runtime uses symbolic evaluation and constraint-solving in order to do this. We have an implementation of Jeeves as an embedded domain-specific language in Scala. (Code here.)

Next steps for Jeeves include looking at how Jeeves can handle policies for integrity and declassification (in addition to confidentiality) and looking ta how well Jeeves scales for real-world applications.

It says a lot about our research community that languages and solvers are at a point where we can even consider this sort of separation of global concerns from core program functionality. I am excited about a future in which we can continue to make programmers’ lives easier by teasing out and automating concerns such as privacy.

Run Your Research in Racket

One of the most fun talks at the Principles of Programming Languages (POPL) conference this year was about Redex, a Racket-based system for lightweight mechanization of programming language semantics. This system allows people to encode their language semantics and theorems in the Racket programming language (the new face of Scheme). The programmer can then play with example programs evaluated using these semantics and use random testing to validate their theorems. This is a much lighter-weight alternative for getting formalisms right than using interactive proof assistants such as Coq. You may read more on the project website.

PLDI 2010 in Toronto, Canada!

I just returned from PLDI 2010 in Toronto, Canada. The papers, talks, and non-technical content were all great!

This year parallelism and concurrency seemed to be the hot topics, as there were two tracks for each of those. According to the program chair Alex Aiken (if I remember correctly), there were relatively high acceptance rates for papers on types, static analyses, and programming language designs. Some papers that I particularly liked include Viktor Kuncak et. al.'s Complete Functional Synthesis about using decision procedures at runtime for synthesizing program expressions, Khoo Yit Phang et. al.'s Mixing Type Checking and Symbolic Execution on a hybrid type-checker/static analyzer, and my adviser Armando Solar-Lezama's Smooth Interpretation with Swarat Chaudhury on smoothing program spaces for analysis/synthesis. The other papers in the verification session with me (Zach Tatlock's Bringing Extensibility to Verified Compilers, Adam Chlipala's paper on type computations and meta-programming with Ur, and Michael Emmi's Parameterized Verification of Transactional Memories) are also cool.

This year they reduced talk length to 15 minutes (instead of 20), which people seemed to have strong thoughts about. The general consensus seemed to be that people appreciated having the time limit for others' talks, as people who worked hard on their talks would take the effort to make a good 15-minute talk, and the short length kept people awake and even enticed people to attend talks on areas of marginal interest. People generally seemed unhappy/concerned about the shortened time for their own talk. Also, someone commented that having shorter talks made them more intense and left less (perhaps necessary) time for zoning out.

This year there was no PLDI-wide outing, but having everyone staying in a huge hotel (Fairmont Royal York) with its own bar, restaurants, shops, etc. promoted PLDI-wide unity. There were also many restaurants and tourist attractions within walking distance, which made it easy to embark on food and other excursions with fellow PLDI-ers. Being by the waterfront was also nice: Tom Ball led a running contingent along the waterfront path every morning at 7am. Before and after the conference, I managed to do a fair amount of sight-seeing: pictures here. (Toronto is huge and has so many interesting neighborhoods! I loved Kensington Market and Old Cabbagetown. Toronto also apparently has multiple Sri Lankan restaurants!)

This was a big conference for me because not only did I give my first conference talk, but my paper with my MSR mentor Chris Hawblitzel (Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System) won the best paper award!

Talk slides below:

PLDI 2010: Safe to the Last Instruction

View more presentations from jxyz.

On collaboration

A friend told me that she was thinking about getting a power couple to mentor her and her boyfriend as a couple. She said that people call her and her boyfriend a power couple because both of them are graduate students with ambitious career plans, and that the fact that both of them are so ambitious worries her because it's difficult to negotiate compromise and determine which fights to pick. This got me thinking about how there is little guidance to have the impressive, synergistic net horizontal* collaborations like these couples have.

I have been thinking about the issue of horizontal collaboration quite a bit in an academic context. While I have gotten advice about how to succeed as an individual and how to navigate the vertical advisor-student relationship, I've gotten significantly less guidance about how to handle situations where there are non-binding commitments between equals. I have been given little guidance about 1) finding someone I can work well with, 2) negotiating a set of goals, 3) negotiating interfaces for working, and 4) actually working with the person (communicating with the appropriate frequency/via the appropriate media, negotiating power and respect, compromising rather than withdrawing--and getting the other person to do the same, etc.)**. I am not even sure if this is the appropriate set of questions to be asking.

There are various reasons why I think people don't tend to give advice about how to enter into successful collaborations. First of all, the degree to which people are good at/enjoy working with others is often accepted as a personality trait that isn't likely to change. Secondly, many people have this ideal of the "lone genius" and believe that smart people do not need to work together. (When I told a professor that I wanted to work on my horizontal collaboration skills, he said I didn't need them because the best people work alone or with their students.) People also have a belief that people who don't work well with others don't desire to work with others. Yet another thing is that in many aspects of life, people don't get to choose who they work with, so understanding how to choose people you work well with and how to work with them isn't the most useful skill to have.

When I told a professor from undergrad about my desire to improve at peer collaboration, she suggested that I approach a peer and do a project in the intersection of our interests. Following her advice, I propositioned my officemate to enter not only into a collaboration (on a programming languages topic in the intersection of our interests, specifics to be decided) but also a meta-collaboration about how our collaboration is going. So far we have collaborated on better understanding the components of collaboration (the spectrum from horizontal to vertical, the size of the interface). Collaborate, collaborating, collaboration, collate***. I will let you know how this goes--I think these lessons will apply to life in general.

Thoughts?

* I refer to vertical relationships as ones with clearly unequal power balance and horizontal ones where the power is equal and neither person's interests or goals subsumes the others.
** I think these things apply to romantic relationships as well.
*** One of these is not like the others.

Programming of the future

Interaction and search allow ambiguity, concision.

Grand challenges in programming languages

This is old news by now, but a couple of weeks ago I was at POPL, where they had a panel on the grand challenges to solve in programming languages. There is a transcript* here.

Simon Peyton Jones said to find a good way to capture effects; Xavier Leroy said continue being awesome with verification; Kathryn McKinley said to keep working on parallelism; Martin Rinard said to question what levels of correctness we want from programs; Greg Morrisett said to think about how to redesign hardware, think about how to program colonies of robots, and think about how to unify PL to educate people.

For fear of beheading I will provide my opinion off the record. :)

* Did you know one summer at Google my entire job was to [accidentally the whole thing]?

Failure-oblivious computing

This is so wild! The goal of program safety as I knew it was: terminate with the correct answer or raise an error. These people at MIT are working on a computing paradigm where instead of raising an error if the program goes wrong, they perform some default behavior. Apparently this works for many things--web browsers, e-mail clients, etc. Read about it here.

image resizing video

holy crap; this image resizing video is amazing. they show how they have targeted resizing of images based on features etc. they can also nicely cut people out of pictures. it sounds boring but it's the coolest video i've ever seen.