Month: June 2015

Conservation of Virtue

Speed Read This
Posted by on June 16, 2015

In Dungeons and Dragons and many similar games, player characters are created with a point system, and have six attributes: strength, dexterity, constitution, intelligence, wisdom, and charisma. Each of these six attributes is represented by a number, and within an adventuring party, while one player’s character might be stronger or wiser or more charismatic, this will always be counterbalanced by a weakness somewhere else.

In the real world, people tend to sort themselves according to awesomeness. They try to hang out with people who are about as cool as they are. Your friends are about as cool as you are; their friends are about as cool as they are. As a result, if your friend introduces you to someone, that person is on average about as cool as you are, too. If you go to the best college you can get into and afford, you will mostly meet people for whom that was the best college they could get into and afford. If you go to the best party that will have you, you will on average tend to meet people for whom that was the best party that would have them.

This produces an odd effect. If you meet someone and find out that they have some significant weakness, this gives you evidence that they have some other strength, which you don’t know about; otherwise, they would’ve sorted into a different college or a different group of friends. Similarly, if you meet someone and find out that they have a particular strength, then this gives you evidence that they are weaker in some other way, for the same reason. I call this effect Conservation of Virtue.

There are three issues with the Conservation of Virtue effect. The first issue is that real people have more than six attributes, and no social dynamic is nearly so precise as a point system with everyone having exactly 75 attribute-points total. Even in a group that carefully filtered its members, you will sometimes meet people who are much more or less virtuous than the average, and if you let the Conservation of Virtue effect inform your intuition, you might fail to notice. And sometimes, you will meet people in ways that aren’t related to any filtering process, so the Conservation of Virtue effect no longer applies.

The bigger issue, though, is that this can make you believe things are tradeoffs when they really aren’t. For example, when I was younger, I noticed the cultural cliche of stupid athletes and smart but weak nerds – and, without ever raising the question to conscious awareness, came to the belief that I could make myself smarter by neglecting fitness as hard as I could. Similarly, I recall a case of someone I know complaining about good reasoners neglecting empiricism, and good empiricists neglecting complex reasoning. Sometimes, false tradeoffs even get baked into our terminology, like “Fox/Hedgehog” (aka generalist/specialist). This is closer to a true tradeoff because building generalist knowledge and building specialist knowledge are at least competing for time, but it is in fact possible to have both generalist knowledge and specialist knowledge; I have heard this referred to as being “T-shaped”.

These confusions can only manifest when things are left implicit. A statement like “I can make myself smarter by neglecting fitness really hard” could never hold up to conscious scrutiny in the presence of real understanding. By giving this effect a name, hopefully it will be easier to notice and to tell when it does and doesn’t apply.

A Broad View of Software Verification

Speed Read This
Posted by on June 7, 2015

Software is terrible. This is mostly okay, except that there are a few specific types of software which we would much rather wasn’t terrible. For example, the software that controls your car’s throttle. Or the software that controls spaceship navigation. Or the first artificial general intelligence, if one is eventually made.

When correctness really matters, we break out the mathematical machinery and formally prove that our software is correct. Or rather, we feel guilty about how we aren’t formally proving our software correct, while academics prove the correctness of toy versions of our software and wonder why we aren’t doing it too. (It’s not like a line count and feature set 10^3 times bigger is a fundamental obstacle).

This is my attempt to outline the problem of making large-scale provably software. At the end of this blog post, you will be ready to apply formal methods to proving the correctness of a large system have an appreciation for why formally proving the correctness of software is hard.

Like most discussions of formal proof in software, we’re going to start with a sort function. This might seem silly, because sorting isn’t that hard, but applying formal proof methods revealed a bug in OpenJDK’s sort function which had gone undetected for years and survived extensive unit tests.

The proof-making process goes like this. First, we define what it means for our function to be correct. In the case of a sort function, that means it takes a list and returns a list, elements of the input and output lists match up one-to-one, and each element of the output list other than the first element is greater than or equal to the element before it. This is the extensional definition of sorting. Then we write the sort function itself, which is a constructive definition: it defines the same thing, but from a different angle. Then we informally prove that the two definitions are equivalent, and then we convert the informal proof into a machine-checkable formal representation.

Consider, for example, this inefficient C++ implementation of selection sort.

int leastElementIndex(vector<int> &vec)
{
int leastElement = vec[0];
int leastIndex = 0;
for(int ii=1; ii<vec.size(); ii++) {
if(vec[ii] < leastElement) {
leastElement = vec[ii];
leastIndex = ii;
}
}
return leastIndex;
}

vector<int> sort(vector<int> input)
{
vector<int> sortedItems;
vector<int> itemsLeft = input;

for(int ii=0; ii<input.size(); ii++) {
int leastIndex = leastElementIndex(itemsLeft);
int leastValue = itemsLeft[leastIndex];
sortedItems.push_back(leastValue);
itemsLeft.erase(itemsLeft.begin()+leastIndex);
}
return sortedItems;
}

Our initial, informal proof goes like this. Upon each entry into the loop, sortedItems is sorted, every element of sortedItems is less than the smallest element in itemsLeft, and each item in input corresponds one-to-one with an item either in sortedItems or in itemsLeft. These are all true on the first entry into the loop because sortedItems is empty and itemsLeft is a copy of the input. If this was true at the start of a loop iteration, then it is true at the end of a loop iteration: sortedItems is still sorted because the item added to the end is greater than or equal to all of the items that were previously there; the one-to-one correspondence is preserved because the item that was removed from itemsLeft was added to sortedItems; and all items in sortedItems are all still less than or equal to the smallest item in itemsLeft because the item that was moved was the smallest item. The loop terminates after input.size() steps, at which point every element has been moved from itemsLeft to sortedItems so that’s the sorted list and we can return it.

This proof is incorrect and the function is not correct either. Can you spot the bug?

This function is incorrect for inputs with size >= 2^31 because input.size() is larger than the largest possible int. When you compile this code, the compiler will give you a warning. This is an overflow problem: when we encounter numbers that don’t fit in a 32-bit int, the things we know about basic arithmetic go out the window. This class of error is pervasive in real programs. An experiment found that most programmers couldn’t write a correct binary search, and this was a major reason. In most cases, the compiler will not catch these errors; our election sort was a fortunate exception.

Unfortunate Primitives

The first obstacle to formal proof is that software is usually built out of primitives that are mathematically inconvenient, creating strange caveats and impedance mismatches. We want integers, but instead we get integers mod 2^32, so n+1 isn’t necessarily bigger than n. This is why we have one less Ariane 5 rocket. We want real numbers, but instead we get floating-point numbers, and suddenly addition isn’t an associative operation. This famously caused the Patriot missile defense system to fail. We either can’t prove that values won’t suddenly change in between accesses, or we have to invest significant effort into proving they won’t, because of mutability. Some languages force us to reason about whether objects have any references left, or else we’ll have memory leaks, or worse, try to use an object after it’s been freed (causing a use-after-free security vulnerability).

Some languages do a better job at avoiding these problems than others. Languages are commonly classified as functional or imperative; the “functional” side is generally seen as doing better at avoiding these problems. However, this distinction is very fuzzy, languages that have traditionally been thought of as imperative and object-oriented have tended to adopt traits that used to identify functional languages, such as lightweight function syntax, garbage collection and immutability.

Static Analysis

Inside every major compiler, there is an inference and proof engine. No, not the type system-the other one. Actually, there’s two proof systems. Type-checking is a sort of proof system, thanks to the Curry-Howard isomorphism; it proves that we’ll never try to do particular silly things like divide a number by a string. But the main inference engine is invisible. Its purpose is to find and prove statements of the form “program P is equivalent to program P’, which is faster”. In most cases, these are independent of programming language and shared between multiple programming languages, and independent of processor architecture and shared between processor architectures.

These proof engines are less ambitious than formal verification in general, but all formal program manipulation starts roughly the same way: by translating the program to a representation that’s easier to work with and easier to prove things about. (Actually, compilers tend to translate programs through a series of representations which highlight different aspects of it, performing different optimizations in each). Because the optimizers in a compiler are entirely automated, and the correctness of their output is important, they don’t get to gloss over any details; they have to thoroughly check their assumptions, including assumptions that would normally be swept under the rug.

When we look at them, we find that many of the techniques are about figuring out and proving things that make good lemmas for a larger proof, such as:

  • Which variable usages correspond to which assignments (SSA form)
  • Which variables/memory locations might or might not change in between accesses (escape analysis)
  • Which pointers/references definitely point to the same thing, or definitely don’t point to the same thing (alias analysis)
  • Upper and lower bounds on variables (value range analysis)

Several of these steps serve to eliminate the differences between functional and imperative programming languages. In particular, the conversion to static single assignment form eliminates mutability in local variables, and the escape analysis reduces (but doesn’t always eliminate) need to worry about mutability in heap variables.

The Dual Definitions Problem

When we wrote a sort function and formally defined what properties we wanted it to have, I phrased this in terms of writing two definitions from two different angles. In practice, this can be the hardest part. There are two ways this can go wrong. First, we might not be able to write a second definition. It was hard enough figuring out what we wanted the first time; if the second specification has to be sufficiently different, we might not be able to do that at all.

This is especially hard if we have components that aren’t well modularized or well factored. Solving it is mainly a matter of good software architecture: identifying the problems your software solves and carving it at the joints, choosing the right joints and carving it cleanly. This is a very hard problem. While some speak of programmers who don’t use formal proof being lazy, this problem is not one that’s usually solved by mere effort; it requires time, deep understanding, and cleverness.

The second problem is that we could write down a second definition, with the exact same error or the exact same blind spot. This is particularly likely for corner cases, like empty lists and extreme values.

Be careful about using the following code — I’ve only proven that it works, I haven’t tested it.
— Donald Knuth

The solution to this problem is unit testing. A unit test is a written example with an expected result. This makes fundamental confusions less likely. It’s also a way of verifying corner cases that would much up a proof. There’s only one empty list, for example, so a unit test on the empty list means not needing to worry about it in a proof. There’s an important caveat, however, which is that a unit test does not necessarily represent a considered belief about what should happen; a developer could cheat, by writing code first, observing what the results are, and then writing unit tests which check for those results, without knowing whether they’re actually correct. This is why Test-Driven Development advocates writing unit tests first, before writing code.

The Complex Interface Problem

CompCert is a formally verified C compiler. It has a proof, verified by Coq, that output assembly has the same semantics as input C programs. Unsure whether it was really for real, I checked its issue tracker. This is unusually good; there are few entries, and almost all of them are new-feature requests. But this one is a straight-up bug, and a fairly serious one. What happened?

What happened was that at the boundary where CompCert-generated code interacts with other compilers’ code in a library, it formats some argument lists differently, causing values to be misinterpreted. This is outside the realm of CompCert’s proof. Applying formal proof to this problem wouldn’t help, because the same problem would show up in the specification used by the proof.

In the case of CompCert, the problem was detected by a modest amount of testing and then fixed. In other cases, however, the interfaces are much larger, and more full of special cases. Proving the correctness of a PDF renderer or a web browser, for example, would be a hopeless endeavor, because what correctness means is defined by others’ expectations about what happens at an interface, and that interface has not been formally specified anywhere.

Conclusion

Formal verification of software is hard, but there is more than one angle to attack the problem from. The first, traditional angle is: write better automated proof-searchers and proof-checkers. But the best proof-checker in the world can’t help if you don’t know what you’re proving, or you’re proving your software does something you don’t want, or you’re building on architectural quicksand. The second angle is purely technical: we need to take the traps out of the core abstractions we’re building on. In 2015, there is no excuse for programming languages to silently wrap integers on overflow, and yet most of them do. And the third angle is: we need to get better at software architecture. This requires improving our cognitive strategies for thinking about it, and looks somewhat like rationality research.

CVEs Per Year

Speed Read This
Posted by on June 5, 2015

If you care about security vulnerabilities that haven’t been discovered yet, then assessing software is hard. It’s very hard to ever convincingly show that something is free of vulnerabilities. There are tools that will help: static analysis and fuzz testing are the main ones. These take a lot of work to use. For high-profile software, however, there’s an easy test to apply first. The Mitre Common Vulnerabilities and Exposures List tracks publicly-disclosed security vulnerabilities, what software they were in, when they were discovered, and how severe they were. If a piece of software has had vulnerabilities discovered recently, it probably has more that haven’t been discovered yet. You can search it here.

This suggests a simple metric: CVEs per year. This is a negative filter; it can show that software is unfit for high-security applications, but can’t show the reverse, because a lack of reported vulnerabilities could just be the result of a lack of attention. With that in mind, here are results for a few important pieces of software. Note that 2015 is only half a year so far (less when you account for publication delays), and the counting process I used is slightly error-prone.

VirtualBox: 3 in 2015, 20 in 2014
VMWare Fusion: 1 in 2015, 3 in 2014, 2 in 2013, 5 in 2012, 21 in 2011-2008
Linux seccomp: 1 each in 2009, 2014, 2015
Linux kernel: 15 in 2015 (at least a few of which would break seccomp but don’t mention it by name)
Firefox: 52 in 2015
Google Chrome: 59 in 2015
Windows 8: 56 in 2015

If things were going well, this would flip from “vulnerabilities per year” to “years per vulnerability”. We have a long way to go.

The Memory Sinkhole Vulnerability

Speed Read This
Posted by on June 4, 2015

On the schedule for the Blackhat conference is a presentation by Christopher Domas titled The Memory Sinkhole – Unleashing an x86 Design Flaw Allowing Universal Privilege Escalation. There’s a discussion going on Hacker News today.

I’m studying the AGI containment problem – that is, how to test and experiment with artificial general intelligences without letting them bypass your safeguards and take over the world. While the development of working AGI is far enough in the future that this particular bug will certainly be fixed by then, this is one the categories of things that keeps me up at night.

The containment system architectures I’ve focused on so far involve layering and defense in depth. You don’t just put your AGI in a VM and call it a day; nor do you airgap it and call it a day. No, you write it in a language with strict semantics, then you put it in an operating system sandbox, that you put that in a virtual machine, and you airgap that. This is necessary both because of occasional security vulnerabilities like this one, but also to enable tripwires and other safeguards; you need the safeguards to be on a sort of high-ground, relative to the AGI, so that they can inspect it and shut it down but the AGI can’t expect them or turn them off.

Only a few details on this exploit are available so far; I’ve only read the one-paragraph synopsis, and I don’t expect more details to come out until August, so the remainder of this post is speculation and prediction on my part.

If I’m understanding the synopsis correctly, this particular exploit is an escalation from VM guest kernel space to host kernel space or system management mode. In the architecture I described, there are two layers of defense (language semantics and process sandboxing) in between the AGI and the point where it could make use of this exploit, and one more layer of defense left (airgapping) after it does. However, the layer it breaks is important, because it’s the last layer protecting tripwires, the integrity of log files, and preventing the installation of BIOS modifications to subvert the hardware after a reset.

Powers That Must Not Be

Speed Read This
Posted by on June 4, 2015

Death Note is a manga by Tsugumi Obha and Takeshi Obata, which centers around a magical book called a Death Note. This book confers a power: by following its instructions, the possessor of the Death Note can kill anyone by writing down their name, and choose the manner of death. The story centers on Light Yagami, who comes into possession of the Note and uses it to kill criminals.

While the story the Death Note is a supernatural artifact, there are things in real life that are somewhat analogous. Assassins have existed for at least as long as recorded history; in a sense, having a Death Note is like commanding a master assassin. What makes the Note different and scary, however, is its anonymity. Real-world assassination is inherently risky and difficult, and it’s risky and difficult every time. This is good; in a world with too many Death Notes, some would fall into the hands of villains, and be used to terrible effect. One reason the world today is a better, safer place than the world of a thousand years ago is because forensic science has made it virtually impossible to get away with murder.

A straightforward extrapolation of currently-existing technologies suggests that this power does exist, and is possessed by a small number of spymasters and heads of state. This is unfortunate, but it’s no worse than it was in humanity’s past.

But there are analogous powers, similar to the Death Note power but not quite the same, which humanity did not used to have, and which we would prefer it didn’t.

One such power is the power of atomic weapons. Rather than killing individuals, these kill regions. Their existence is a large and obvious threat to everyone, but fortunately, they are hard enough to make that only governments are able to acquire them, and their terribleness is imprecise enough that no government is willing to use them; the ensuing disaster would affect them as well.

There are other powers, which are worse, which technology hasn’t brought into the world yet, but might. Consider what happens in a world where internet-connected drones are common. Drones are dangerous; they can kill people by crashing into them. What happens if they’re hackable?

The combination of bad computer security, face recognition, and hazardous internet-connected devices could create a Reference Class Note: an artifact like Tsugumi’s Death Note which, instead of targeting a person, targets an arbitrary category of people. And the nature of computer software is unfortunately not like the nature of fissile elements; hazardous software can be constructed by skilled individuals.

There are other ways this could happen besides drones, which I will not name. What all of them have in common, though, is that they depend on the continued failure of computer security. In the 90s and early 2000s, cracking computer security was within easy reach for bored teenagers; they used this power for pranks, and were the first canary in the coal mine. Today, the bored teenagers mostly can’t manage it, but skilled individuals can; they use this power for theft, and are the second canary. We need to drive the bar up higher, to the point where defeating computer security is limited to large organized groups. We need to do this soon, before the “Internet of Things” takes hold.

If we can’t? Bam, sci-fi dystopia.

Technological Unemployment

Speed Read This
Posted by on June 3, 2015

Will automation displace workers and eliminate jobs? For many jobs, yes. Whether this will cause unemployment, however, is a controversial and open question. When technology automates away jobs, there are several possibilities for what happens to the people who would otherwise have been in those jobs. The total number of jobs worked might drop, or they might just shift to doing jobs that are hard to automate. If the number of jobs worked does go down, this could lead to people being unemployment and impoverished, or it could instead result in people entering the work force later, retiring earlier, working part time, and taking more long vacations.

Predicting what will happen is hard. Noticing what already happened, however, is more straightforward. Automation is not a new force in the world, and technology-driven unemployment has been a concern at least as far back as the Luddite movement in 1811. With the benefit of hindsight, nineteenth century Luddism was clearly incorrect; there was a massive amount of important work left undone for lack of people to do it. But what about more recent trends? Here from the Bureau of Labor Statistics is the United States unemployment rate, for everyone aged 16+.

Bureau of Labor Statistics Unemployment Rate, 1948-2014

This graph displays a pattern best described as “glaringly absent”. It’s basically noise. Why? It turns out that the definition of unemployment is fairly complicated. Unemployed refers to people who are jobless, available for work, and looking for work; it excludes people who have tried to find work recently but aren’t currently trying (marginally attached workers), people who have given up on finding work (discouraged workers), students not looking for work, and people unable to work because they are ill or disabled. The “discouraged workers” category is particularly unfortunate; it means that the unemployment rate is measuring a sort of residual, the people who can’t find work but haven’t realized it yet. A much more straightforward number is the employment-population ratio. This is simply the number of employed people divided by the population. So here, also from the Bureau of Labor Statistics, is the United States Employment-Population Ratio, for the civilian noninstutitional population, age 16+. (Excludes people on active duty in the armed services and prisons, nursing homes, and mental hospitals.)

Bureau of Labor Statistics graph of employment-population ratio, 16+, 1948-2014

This graph gyrates a little less wildly. If you squint hard enough, you might fool yourself into seeing a pattern. It turns out there is one more confounder to separate out.

Paul Samuelson famously criticized GDP by observing that, if a man married his maid, GDP would fall. In fact, it’s not just GDP that would fall; employment would fall, too. Employment only counts work that is done for wages; there is a separate category, “household activities”, for the rest. This includes things like cooking, laundry and child care. Unfortunately, this time the BLS doesn’t have a nice graph to give us, but we can get a few point estimates. The American Time Use Survey estimates that household take an average of 9.5 hours per week for men, 15.5 hours per week for women. By contrast, Valerie Ramie in the Journal of Economic History reviews twelve estimates from 1924-1953 and finds that in that time period, homemakers spent 47-63 hours per week on household production – a time expenditure comparable to or greater than that of full-time employment. This household labor fell primarily on women, and has now been substantially reduced by inventions such as laundry machines, microwaves, and robotic vacuum cleaners, as well as by declining fertility. This combined with changing social norms caused many more women to enter the labor force, as shown by the employment-population ratio for women:

Bureau of Labor Statistics graph of employment-population ratio for women 16+, 1948-2014

Here we see womens’ employment increases until some time around 1990-2000, then either stops changing or starts falling. This comes partially at the expense of mens’ employment, but I think it’s mostly at the expense of household activities. Meanwhile, the employment-population ratio for men looks like this:

Bureau of Labor Statistics graph of employment-population ratio for men 16+, 1948-2014

This is a steady decline of about 2.7% per decade. To see whether this trend extends past the time range covered by the BLS time series, I also checked the 1910 census and found that the employment-population ratio (male 16+) was 91% (Final Report Vol. 4 Ch. 1 Pg 69).

Based on this data, I expect both the US male and female employment-population ratios to decline at about this rate in the future. This will manifest as a mix of people entering the work force later, retiring earlier, working less, being declared legally disabled at a lower threshold, and sharing income within families. Depending on policy and social norms, we could have more leisure for everyone, or more poverty, or some mix of the two. It’s up to us to choose wisely.

The Failed Economics of Devtools and Code Reuse

Speed Read This
Posted by on June 2, 2015

Why do so many people and so many projects use PHP? Why is there so little code reuse, so few high-quality libraries and development tools to build on? There are several reasons, but one that hasn’t received attention is a problem in the economics.

When starting a new project, the creator picks a programming language and a set of software libraries. Consider the case of a developer starting an open source project, and choosing between an inferior tool with low up-front cost, and an overall-superior superior tool with higher up-front cost. The better tool might cost money, or it might just have a learning curve. Which will they choose?

Developers of open source projects hope to attract collaborators in the future. Unfortunately, most of the costs of a development tool or library are borne not by the person who chooses it; they are borne by the future collaborators who they hope will materialize later. While an existing collaborator might agree to learn a new programming language or pay for a new tool, a hypothetical future contributor can’t do that. Attracting volunteers to work on an open source project is very difficult to begin with, so developers are strongly averse to imposing costs on them. The perceived impact of these externalized costs is magnified many times over, so people don’t accept them.

You would think a company building a team to work on a software project wouldn’t have this problem, because it can internalize the future costs: it pays for the software and it pays employees for the time they spend getting up to speed. But there’s another problem. The quality of a software library is hard to judge until you’ve used it in a project; it’s risky to try an unfamiliar library in a big company-funded project with a team. So developers try out new libraries in smaller, less-important projects where they can take risks — and these tend to be open-source projects, where trying new libraries is a low-ranked side-goal.

This results in an equilibrium where people reject tools, not because they themselves are deterred by the up-front cost, but because they expect other people to be deterred by that cost. This means that if you write a better IDE, a good library, a better compiler, or some other piece of superior software, you’ll have a much harder time charging money for it than the direct economic proposition would suggest, and a much harder time getting people to try it and learn how to use it than the direct economic proposition would suggest.