Category: software security

From comments below.

Just one more comment: I think we should make a distinction between a tool that can verify threaded code and a tool that can verify the code that implements threading. The latter is what you are looking for here and it is much more difficult. Furthermore it is arguably unnecessary — a reasonable engineering solution is to get someone really good to write the dispatcher/scheduler and then focus verification effort on the mountains of code written by the rest of us that run on top of that core functionality.

I’m not so sure about that. The example below uses threading primitives – it does not implement them. We could even look at a more academic example and see the same problem.

threadA:
    while(1){
                  x = x+1;
                  sem_post(&z);
                  sem_wait(&t);
                  y = y+1;
   }
}
threadB:
   while(1){
       y = y+1;
       sem_post(&t);
       sem_wait(&z);
       x = x+1;
     }

My 20 second inspection tell me this ultra-simple example is right (which means it may have 100 errors). Prove it without having enough machinery to do the code below.

Updated below!

Years ago I proposed the following code snippet as a minimal standard for a useful verification method. Still not quite there.

/* you are not expected to understand this */

if(save()){

          load_memory_management(); /* map in new current */

          return;

}else {

         current = new;

        resume();

        panic("RESUME RETURNED! KERNEL BROKENn");

}

Not so complicated, but if you can’t do this, you cannot handle operating systems at all- or any threading.

In response to the comment. This is a paraphrase of Dennis Ritchie’s  Unix switch code and comment.  “Save” saves the registers and the return address for “current” and always returns 0. “Resume” restores the saved registers and return address for current (by doing so, changes stacks) and returns 1 – to that saved return address which is the test of the “if”. So the “if” statement is always evaluated as false when saving and is always evaluated as true when resuming and “resume” never returns to the else.  I always took Ritchie’s comment to be a warning that the code and the previous comments were not easy to understand. The state change here is basic thread switching but it is slippery.

[fixed a couple of typos, Dec. 20 2007]

John Regehr writes:

On the other hand, there is plenty of useful work to be done on supporting time sensitive applications (I’ll just avoid saying “soft real-time”) even when no guarantees are made. Let’s take the example of an OS that disables interrupts when any process is executing inside the kernel. This is not hypothetical, I was recently talking to people designing such an OS because they are formally verifying it; they did not believe they were capable of verifying an OS that accepts interrupts more liberally. Anyway, needless to say the average-case response time to interrupts of this OS will suck. Now if we have some breakthrough in verification that permits interrupts to be accepted most places in this kernel, average case responsiveness will improve though worst-case may
not. Is this useless? Of course not, if it makes it possible to watch videos or listen to music or similar, on this OS. For applications of this kind a mathematical guarantee is simply overkill and what we really care about is more like “works almost all of the time in practice, given actual workloads.”

This is perfectly reasonable, in fact, there are many interesting properties of operating systems that are not real-time properties at all if we define real-time properly so that it does not end up meaning “any performance properties.” What’s unreasonable is this idea that crippling a piece of software to make it possible to “prove” that it “works” gains much of anything. That story about the drunk looking for his keys under the light-post is supposed to be a joke, not a design methodology. It’s fine to argue that by simplifying a system one can validate it while not losing too much performance or functionality for the purpose – but all too often the second part of the argument is omitted. What is the point of a system that is provably “correct” at a performance level that assures it cannot be used for its ostensible purpose? Worse, this methodology is often used in order to make it possible to apply “mathematical” methods which have not been ever shown to be more reliable than testing or code reviews or even good luck charms (the claim that “formally validated code is better than other code is, at best, unproven).

The phrase “mathematical guarantee ” is worth some deeper analysis.

• Mathematical. The types of “hard specifications” that I am advocating do not need to be overly “mathematical” and certainly don’t need to be “formal” to be useful. On the contrary. The “formal methods” advocates have made a fetish of formalization to the detriment of useful engineering specification and that causes people to shy away from attempting to be more precise. What we want from a specification, at minimal, is that it should be falsifiable. Perhaps an incremental approach to adding fast paths to operating system services to reduce interrupt latencies can make the system described above “more responsive” for “standard workload”. If so, we should be able to characterize “more responsive” in some falsifiable way. If the specification is just “there is no wall-clock observable delay on the echoing of typed characters while stress program S runs in the background and a tester types a file in the ed program” or that “programs A,B, and C start within 5 seconds of double clicking the icon” then it is at least a falsifiable specification and is a concrete goal for the software developer. In any case, we can see that “average” is not what is needed, since “average” implies that if the system runs for 1 hour, a 5 minute total stop can be amortized away by 55 minutes of high speed operation. Perhaps what we want is as simple as “the video player on an otherwise unloaded system will not stop more than 10 seconds cumulatively over a one hour period where stops are delays in frame display that are over 1/60th of a second.” But this “soft” real-time requirement carries a real-time property with it – as argued previously.
• Guarantee. There is a difference between a design guarantee and an evaluation guarantee. A TCP/IP network stack is designed to produce an in-order, reliable, stream of data between sender and receiver. But it is possible that in some situations, under some loads and with some definition of “reliable”, a simple datagram stack can produce the same property. The TCP/IP stack is designed to guarantee a property that the simpler stack may be shown to have in some circumstances. An evaluation guaranty is an attempt to show that a system has some property. One of the most useful ideas in Common Criteria is the evaluation assurance level (EAL) which is supposed to indicate the reliability of such a guaranty. One might find “we ran it a couple of times and it looked good” to be less or more reassuring than “we produced a 300 page document that strenuously exercised the symbol production features of LaTex” but these are both “evaluation guarantees”. Note that design guarantees should be backed up by evaluation guarantees that the design is correct and implemented correctly.

“Real-time software” normally refers to software that offers design guarantees on latency and scheduling times, data rates, or other time sensitive operations. Validating that the design succeeds requires some combination of testing, mathematical proof, and design and code review. But we may also be able to validate real-time properties of code that has no design real-time properties at all. One could take an instance of a LAMP stack (Linux + Apache + MySQL + PHP) and subject it to extensive testing on a particular hardware platform and observe that in practice it satisfies a real-time specification. Suppose our measurements show that all pages of a certain limited complexity will be “served” within 1 second over a 1GB network that is reserved for the LAMP system and where requests are at a rate bounded by R and there are no more than 30 seconds cumulative failure on this property over 1 hour. That’s a falsifiable, concrete, real-time specification – mathematical, even [this is in response to a note from B., a very knowledgeable system designer who may or may not be quotable].

Via Schneier comes a story about the US Navy and a disgruntled contractor who just plead guilty:

He confessed to programming malicious software codes into computers that track Navy submarines in May 2006 while in Naples. He told Navy investigators that he was upset that his company’s bid on a project was passed over. Sylvestre had fled Italy after he entered the codes.

The guilty party, one Richard Sylvestre, was a sys-admin at a US Navy System based in Naples Italy and he had a top-secret security clearance. So, without being to crass about it, the sales pitch about security as a property of who works on the software is once again shown to be simply ridiculous – see my old note on the subject. Security is a reliability issue that needs to be addressed in design and administration procedure. The network that was hacked was too trusting of its operators and the people who were responsible for administering the sys-admins were not doing their jobs.