Proving a Computer Program's Correctness

This is interesting:

Professor Gernot Heiser, the John Lions Chair in Computer Science in the School of Computer Science and Engineering and a senior principal researcher with NICTA, said for the first time a team had been able to prove with mathematical rigour that an operating-system kernel—the code at the heart of any computer or microprocessor—was 100 per cent bug-free and therefore immune to crashes and failures.

Don’t expect this to be practical any time soon:

Verifying the kernel—known as the seL4 microkernel—involved mathematically proving the correctness of about 7,500 lines of computer code in an project taking an average of six people more than five years.

That’s 250 lines of code verified per man-year. Both Linux and Windows have something like 50 million lines of code; verifying that would take 200,000 man-years, assuming no increased complexity resulting from the increased complexity. Clearly some efficiency improvements are required.

Tags: , ,

Posted on October 2, 2009 at 7:01 AM • 91 Comments

Comments

pdf23ds • October 2, 2009 7:19 AM

Technically, it hasn’t proven to be “bug-free”. Part of proving program correctness is picking properties about the code to prove. If they overlooked even trying to prove some important property of the code, then it could still have unforseen problems. However, it’s a great accomplishment. They’ve proved that it’s free of certain classes of bugs that they knew to look for, which presumably cover most common failure modes.

What I’d like to know is how many bugs in the kernel source they found and corrected in the process of proving correctness.

Tom Welsh • October 2, 2009 7:46 AM

An entire Linux distribution may amount to 50 million LOC, but that can easily be broken down into separate programs and components (because that’s how proper softare is designed). Then the programs and components could be verified one by one, starting with the most important and those upon which other software depends.

JRR • October 2, 2009 7:59 AM

Clearly we need to build a computer program that can mathematically prove the correctness of other computer programs. Then we simply need to mathematically prove the correctness of that.

Jl • October 2, 2009 8:02 AM

Yup, it’s only as secure as the properties you’ve defined and proven.
Furthermore, large math projects often contain errors: Don’t be surprised if, under closer scrutiny, someone finds a fault in their proofs.

Because of the Halting problem, termination of programs written in a turing complete language is not provable.
And no OS can recover from all possible hardware failures.

THAT SAID:
If the core of the OS has been proven to have many strong properties, e.g. it can’t crash under reasonable hardware assumptions, then building a more complex (and well tested!) OS on that proven core could be very profitable!

So congrats to the team and let’s see what we can build on their work.

Frank • October 2, 2009 8:03 AM

My experience with testing that I ahve seen with large code producing vendors is that they go with standard cases to test. In the year 1990 nobody was thinking of testing against buffer overflows. So does this method scale to address for the currently unknown? Reminds me of the guys producing “ants” to tackle malicious code. They already have 3000 different ants but where does it stop? Suddenly 30,000 ants are in your network or you spend 10 years to proove your code is bug free.

Dave Walker • October 2, 2009 8:03 AM

…lest we forget the Viper chip – proven correct, yes, but practically, almost useless.

Also, I can’t help but roll the classic Knuth quote out – “Note that I have not tested this code, I have merely proven it correct”.

Tim • October 2, 2009 8:09 AM

This page has the answers to any questions people will ask here:

http://ertos.nicta.com.au/research/l4.verified/proof.pml

In particular:

“We mentioned above that our formal proof of functional correctness implies the absence of whole classes of common programming errors. Provided our assumptions above are true, some of these common errors are:

* Buffer overflows
* Null pointer dereferences
* Pointer errors in general
* Memory leaks
* Arithmetic overflows and exceptions"

Apparently they are all impossible in seL4.

pdf23ds • October 2, 2009 8:10 AM

Furthermore, large math projects often contain errors: Don’t be surprised if, under closer scrutiny, someone finds a fault in their proofs.

Well, these are all computer-checked proofs, so there can’t be any errors in the proofs, though there could be errors in the formulation of the theorems, or, very unlikely, in the axioms.

Because of the Halting problem, termination of programs written in a turing complete language is not provable.

That’s only true in the general case. It’s trivial to prove the termination of many programs. I would guess that it’s possible to implement any computable algorithm that always terminates in a manner that can be proven to terminate.

aikimark • October 2, 2009 8:14 AM

Even the simplest programs are not immune from defects. In OS/360, one of the simplest programs, IEFBR14, had to be patched. One tale I heard was that it was the first patch every issued — and the program is only 4-6 lines of assembly instructions!

==========
@JRR

I’m not sure that this is possible, given the work of Alan Turing (et. al.).

AlanS • October 2, 2009 8:18 AM

@JRR
Agreed. See writings by Michael Mahoney, an historian of computing at Princeton, on ‘sofware engineering’ and mathematical theory in computing science.
http://www.princeton.edu/~mike/computing.html

From ‘Computer Science: The Search for a Mathematical Theory’:
“Efforts to bring mathematical rigor to programming quickly reach a level of complexity that makes the techniques of verification subject to the very concerns that prompted their development….computer science remains an amalgam of mathematical theory, engineering practice, and craft skill.”

christopher • October 2, 2009 8:25 AM

The best way to think about this is: proving a program correct means it matches your design. If your design is flawed, your program is equally flawed, but it is still “correct” since it matches spec.

Tim • October 2, 2009 8:28 AM

Furthermore, pdf23ds:

“How many bugs have you found?

We found 160 bugs in the C code in total. 16 of these were found during testing and internal student projects running the kernel before the C verification had started in earnest. 144 bugs were found during the C verification phase.”

JP • October 2, 2009 8:41 AM

“Because of the Halting problem, termination of programs written in a turing complete language is not provable.”

No, it’s impossible to write a program that, given a second program as input, can determine whether the second program will terminate.

It is, however, entirely possible to prove that individual programs will terminate.

David • October 2, 2009 8:46 AM

It’s also worth noting that this is a proof of certain correctness properties for the C code. The assembly language code involved was not proved correct, and the translation and loading of the C code was assumed correct.

This is a very impressive achievement, but the relatively limited results show that formal code verification is very, very difficult.

My personal experience with formal correctness proofs is that it’s possible to prove small things correct (which can be very useful), and once I’ve proven something correct the only errors tend to be the really stupid kind that are easy to find and fix.

Pete Austin • October 2, 2009 8:57 AM

In the real world, “100 per cent bug-free” does NOT mean it’s “immune to crashes and failures”.

kangaroo • October 2, 2009 9:01 AM

JP : “No, it’s impossible to write a program that, given a second program as input, can determine whether the second program will terminate.
It is, however, entirely possible to prove that individual programs will terminate.”

A proof is equivalent to writing a program. So, to say it more correctly, it is possible to write a program that can determine the termination of a sub-class of other programs — just not all classes of other programs (including the class of programs that your proof belongs to).

The sub-class would then have to not belong to the class of programs that can fully implement Principia Mathematica — it would be the unGodelizable set of programs.

Now, Turing-complete is basically isomorphic with Godelizable — one is the programming idea, while the latter is the formal systems idea. So, we’re talking about programs which are unable to to interpret a Turing-complete language — even if they were written in one.

So, to go beyond simply proving a subset of the properties of a program, but instead “prove” the given program in general, the program would have to be a pretty simple one — one that, in short, is incapable of modifying itself in general. Most kernels and computer systems are — in general, they’d be pretty damn useless if they couldn’t.

Of course, there is a way around all that — because in fact all real computers have finite memory. So you could iterate through all the states of the program and determine all the programs properties. So, you can trivially show that a brute force approach exists for the subset of programs that will actually run on a given real computer (since no real computer is actually Turing complete).

sp332 • October 2, 2009 9:04 AM

@JP:
“It is, however, entirely possible to prove that individual programs will terminate.”

How are you going to prove that? You would have to write a Turing machine that takes that program as input and proves whether or not it halts. So no, you can’t prove that any given program will terminate.

Aguirre • October 2, 2009 9:07 AM

“the code at the heart of any computer or microprocessor—was 100 per cent bug-free and therefore immune to crashes and failures.”

We fired the microprocessor up and ????

It got a soft error caused by a nasty little cosmic ray.

More lead shielding required.

Mike Sperber • October 2, 2009 9:09 AM

Elsewhere, huge strides are being made wrt. efficiency, given that a lot of research is going into proof-assistant software. In the CompCert project, proving about 6000 lines of a compiler (for a large subset of C) took Xavier Leroy about 3 years.

http://compcert.inria.fr/

JP • October 2, 2009 9:16 AM

“So no, you can’t prove that any given program will terminate.”

To be more clear, given a single, specific program, it may be possible to prove that it terminates. (In other words, you can write a program that, given another program as input, will output “terminates”, “does not terminate”, and “cannot determine”.)

paul • October 2, 2009 9:25 AM

Where is the cost? If in the translation of code into logical specification and vice versa, you’re sunk. But if it’s just prover cycles, Moore’s law should be helping on that.

Adam • October 2, 2009 9:27 AM

@sp332

No, you don’t need to go to a Turing Machine in this case. The key word here is “individual”. The point about Turing Machines is a subtle one in that it only refers to the general case. A single program can be proven correct manually if it’s within a very small size. You can look up unassisted proofs that quicksort terminates.

For larger programs, you need a machine to help you. The general technique is to come up with a set of small-but-useful theorems that you can prove to be true manually, then construct your proof in terms of those theorems. This may be a poor analogy, but the technique is vaguely similar to applying functional decomposition to standard programming problems.

You quickly hit a point where you need machine checking to make this kind of proof manageable, but if you’re smart about it (and these guys are) you don’t leave any unreasonable assumptions unchecked.

Paul Crowley • October 2, 2009 9:56 AM

“Because of the Halting problem, termination of programs written in a turing complete language is not provable.”

I can prove that this program terminates:

int main(int argc, char *argv[]) {
return 0;
}

gilberto • October 2, 2009 10:11 AM

IEFBR14 is just 2 assemby instructions: set returncode to zero, then return to calling program. it really does nothing, but functions as a place holder for IBM MVS/zOS operating system to do file allocations, within MVS JCL scripts, so it is not a good example or benchmark in this case. as for the halting problem: you can not write a universal program UP, that can determine if ANY given inout program P halts. The key here is that UP has to work for ALL input programs, but clearly there are many programs small and large that can be shown to terminate.

Curt Sampson • October 2, 2009 10:21 AM

There was a presentation on this given at ICFP last month. Searching for “Experience Report: seL4 — Formally Verifying a High-Performance Microkernel” will bring up all sorts of links to the paper and its related research; the video is available at http://vimeo.com/6628930 .

For those who haven’t followed up on the details, the proof was quite a lot of work. They proved about 7000 lines of C code, but the proof is about 150,000 lines of code (which is machine-checked).

Note that proving certain properties of code (as opposed to testing, which, as Dikjstra so famously said, can only show the presence of errors, not their absence) is something that many programmers have been doing in a limited way for a long time: that’s the whole point of a type system. Languages like Java, unfortunately, have rather lame type systems and so don’t let you prove very much at all (and often what you can prove isn’t of very much use), but there are far more powerful systems out there, and in fact that is, at least in part, what systems like Isabelle (which is what was used to prove this OS kernel) provide.

Jo • October 2, 2009 10:22 AM

Paul says:
“I can prove that this program terminates:

int main(int argc, char *argv[]) {
return 0;
}
”
Sure – and I can prove my “hello world” program terminates as well (unless I put in that ‘goto 10’ line at the end…). But do you have an algorithm for proving that an arbitrary program terminates?

Of course- proving termination (or non-termination) is not the same as proving there are no bugs, nor is it: “mathematically proving the correctness of about 7,500 lines of computer code”. And what I really want to know is what was proven? It sounds like what was proven was that the code will not allow several classes of faults to occur – but is that ‘correctness’? (Note – ‘correctness’ sounds to me like the syntax is correct and when I run it through gcc, I get an a.out that does something approximating what I wanted it to do).

Then there are the inevitable tradeoffs – by preventing these types of errors, are there things that the computer cannot now be programmed to do (using that OS)? I don’t know – just throwing the question out there…

ex animo omnes-

Alan Braggins • October 2, 2009 10:47 AM

Well, these are all computer-checked proofs, so there can’t be any errors in the proofs

Not strictly true, since there could be errors in the checking code (including the operating system it runs on), or errors in the design of the hardware it runs on.
Bootstrapping an entire verified system from designs which are simple enough to reliably verify manually would be a truely huge task.

Early IEFBR14 history is described on http://en.wikipedia.org/wiki/IEFBR14#History_from_the_RISKS_Digest

There are implementations of /bin/true with comparable revision histories.

o.s. • October 2, 2009 11:06 AM

I’m quite interested in formal software proofs but I don’t know if it will ever become a practical exercise. For example, a simple program with just 32 if statements already has 2^32 unique states for true and false across those 32 if statements. So already the task of correctly verifying the simplest of programs can become huge.

Adam • October 2, 2009 11:08 AM

Does it matter whether we can prove Windows is bug-free? We’ve already proven that it isn’t bug-free.

Joe Buck • October 2, 2009 11:52 AM

“Because of the Halting problem, termination of programs written in a turing complete language is not provable.”

Incorrect. It only means that any correct procedure to try to prove whether programs halt must give three-way answers: it halts, it doesn’t halt, or it can’t be determined.

Optimizing compilers have to “solve the halting problem” in this sense all the time.

-ac- • October 2, 2009 12:00 PM

Great to have a framework like this. It would be interesting for a team to build a new OS using this framework as they went. Say, a smart phone OS.

But the microprocessor code would obviously more fundamental.

Pascal Cuoq • October 2, 2009 12:03 PM

To answer a few recurring misconceptions in the comments:

  • yes, NICTA’s work does not protect us from bugs in the specifications. Do the usual human methods of testing and code reviews make us safe from bugs in the specifications? At least in seL4 there are some classes of bugs that cannot happen.

  • no, it is extremely unlikely that a bug will be found in the proofs, because the proofs are machine-checked. Bugs can be found at the interfaces (i.e. specifications and axioms). Again, do code reviews protect us from flawed assumptions in the reasoning of humans involved in the process? At least with seL4, all the hypotheses are written down so you can examine them for yourself.

  • some programs can be proved to terminate. Some programs can be proved to be bug-free for a non-trivial definition of “bug”. This one has. This does not contradict Computability’s principles in the least.

  • Heck, even some uses of Skein-256 can be proved to be bug-free, for a limited but still not trivial definition of “bug”: see tutorial in http://frama-c.cea.fr/download/value-analysis-Beryllium-20090902.pdf

anonymous • October 2, 2009 1:22 PM

Bruce, seL4 is a microkernel. Most of what’s in Linux would go in the userspace. Unless your claim is everything down to the text editor should be formally verified, this is going to have a great deal of practical effect. If you’re curious, there was an attempt to make a low level language to allow easy verification proofs: http://www.bitc-lang.org/ .

Pascal Cuoq • October 2, 2009 1:31 PM

@Nzruss Interestingly, Airbus used comparable methods to satisfy some DO-178B objectives for some of the level A code of the A380.
Sorry that the link is in French, but in the world of embedded code, you have to do with what you have:

http://www.captronic.fr/documents/trophees/trophees-2009/trophees-embarque-2009-laureats.pdf

(they published more information in English themselves at ERTS or similar venues)

Bruce mentions the “250 lines of code verified per man-year” ratio. An interesting question is how much does it cost to obtain near-complete confidence in a piece of code (say, level A code) using tests and code reviews. Apparently, about the same, since for some problems formal methods come out ahead (Airbus does not use formal methods by ideology. They use them because they think they can get a competitive advantage this way).

Anthony DeRobertis • October 2, 2009 2:12 PM

The halting problem is for universal Turing machines. No such thing has ever been built nor, within the known laws of physics, is such a thing buildable. Computers are finite state machines (assuming we’re talking a computer with no true random number generator).

It’s “easy” to prove if a finite state machine halts. Keep running it, writing down each state it enters, until you either (a) hit the halt state, in which case it clearly halts; (b) hit a state you’ve seen before, in which case it does not halt, ever.

Of course, actually doing that isn’t possible, because the number of states is far too large. But, mathematically, its possible.

Clive Robinson • October 2, 2009 2:27 PM

A simple question to ponder,

Do I care if the OS is provably bug free provided it has a mechanisum which recognises errors and exceptions and handels them in a sensible way?

As has been noted “nothing in life is perfect” but we still manage to get things done (ECC’s work wonders for more than unreliable communications).

Another thing is if we assume for arguments sake the kernel is sufficiently robust, when are we going to se a security hypervisor for it.

Random Walk • October 2, 2009 2:33 PM

Termination can certainly be proven for many programs, however, an operating system kernel does not necessarily need to terminate !

Nick P • October 2, 2009 2:50 PM

Actually, seL4 isn’t totally verified yet. All of the C code is, but several hundred lines of x86 and ARM assembler aren’t. One of the next phases is a correspondence proof of the ARM assembler, as the technology will be used on cell phones by OK Labs. It will likely be integrated into OKL4, already excellent product.

Clive, you should care. None of those “error-tolerant” systems can protect your private key, prevent a drive-by-download from disabling your firewall, etc. seL4, which I’ve posted about many times here, is a MILS architecture kernel that isolates critical apps from main system. It currently has paravirtualized Linux, and the OKL4 and seL4 microvisors allow one to use drivers in any of the partitions. The small TCB and formal proof provide extreme confidence in it.

Want to see a security hypervisor for it? It is a separation kernel, which is useful enough in some situations. It IS a hypervisor for Linux apps. It runs on x86 and ARM. If you want to get started, download and play with OKL4. It’s used in many cell phones right now. They are gradually transforming OKL4 into seL4: it will be at its core, or offered as a separate product.

Personally, I’m very excited about this and I anxiously await both the separation kernel and the development/porting of high assurance middleware.

Rik, UK • October 2, 2009 3:01 PM

It seems that people like to comment on the Halting Problem, many citing Turing Machines, despite the fact that they have obviously not read Turing’s work. Perhaps they would find the earlier work carried out by Church easier to understand?

The works by Church and Turing rely solely on mathematical proofs. No mention is made of computational automata.

I do wish that people who work in IT would stick to IT and not pretend that they are computer scientists.

pdf23ds • October 2, 2009 4:11 PM

Impossibly Stupid, your name is pretty much right. The Pentium FDIV bug was present before Intel starting using formal verification for their processors, and in fact, the bug is what caused them to start doing formal verification.

I simply can’t believe how many people in this thread keep flogging dead horses. Five different people all saying the same mistaken bullshit about the halting problem, and twice as many people correcting them. Several people pointing out the possibility of bugs in the proof verifiers, even though it’s extremely unlikely. It’s like no one read the first ten comments.

David • October 2, 2009 4:27 PM

@Anthony DeRobertis: It seems symmetric to me. Mathematically, you can’t necessarily predict if a Turing machine (which is a mathematical construct) will halt. Practically, you can’t necessarily predict if a practical computer will halt.

David • October 2, 2009 4:40 PM

pdf23ds: Have the proof verifiers been proved correct, and are we sure that proof is correct? If not, then we are entitled to suspect the verifiers might be buggy.

‘I would guess that it’s possible to implement any computable algorithm that always terminates in a manner that can be proven to terminate.” Certainly, for any program that terminates there is a program with the same output that provably terminates, but I don’t think that’s what you mean. I can write a computable algorithm for testing Goldbach’s Conjecture that either will or will not always terminate. (My guess is that it doesn’t, but I can amass enough unproven conjectures so that by sheer chance I’ve likely got one that terminates.) You’re not going to be able to solve these by determining which algorithms terminate.

anonanona • October 2, 2009 5:03 PM

@David

“pdf23ds: Have the proof verifiers been proved correct, and are we sure that proof is correct? If not, then we are entitled to suspect the verifiers might be buggy.”

And you might as well say, “What if the hardware on which the proof was run were buggy? Then the output is suspect!” My only response is, it is easier to check for errors in one verifier than it is to check for errors in multitudinous programs.

The link posted above by Tim I will repost here because obviously many of you have not read it:

http://ertos.nicta.com.au/research/l4.verified/proof.pml

Read it as it addresses many of your critiques.

Nick P • October 2, 2009 5:05 PM

@ David

The first line of your recent post shows the most important issues. The 1st issue, proving the prover, is largely solved. When proving, one goes for a “sound” prover. Those like Isabelle have at their core an easily verified, very sound logic. It makes their results believable. Quite honestly, building on a hand-verified core based on formal logic is probably the best we can do there. Now onto the 2nd issue…

@ pdf23ds

I’m one of the guys who actually read the comments and many papers, like Guttman’s, on where formal methods screwed up. Many, MANY cases of it. The 2nd issue david mentions is responsible: problematic proofs. Proofs can be machine checked but very wrong.

The real-world system must be modeled accurately, and with the right amount of granularity. Issues with the prover, like inability to represent infinity, must be properly accounted for. In process of creating intermediate proofs, one mustn’t abstract away important properties. It’s all very tough and there still is no real standard methodology for doing it. Everyone is constantly inventing new tools, new logics, new approaches, using different programming languages etc.

All this nonsense about halting problems and stuff aside, are you at all surprised at the skepticism by some comments? I mean, mathemeticians have been screwing up simple proofs for well-understood phenomenon for years. This is a 100,000+ line proof of a complex system using brand new models of Haskell and C. While NICTA and UNSW is renown for quality and I’m a big fan of this, even I would like to see some VERY thorough independent review of those big ass proofs. Isn’t complexity the enemy of security? Where’s the “code review” of these proofs? Or even the code itself, which isn’t released?

rjh • October 2, 2009 5:05 PM

@pdf23:

“I would guess that it’s possible to implement any computable algorithm that always terminates in a manner that can be proven to terminate.”

By definition, algorithms terminate. That’s one of their properties. See TAoCP Vol 1, page 4; algorithms always terminate. By the Church-Turing conjecture, all algorithms are computable. So let’s rewrite this as, “I would guess that it’s possible to implement algorithms in ways that can be proven to terminate.”

The Curry-Howard correspondence connects proofs of correctness with implementations in some pretty deep and surprising ways. If you can prove it’s an algorithm, then you compile your proof and you’ve got executable code.

So you’re right, yes — I’m just not sure what you were trying to say. It seems pretty tautological.

pdf23ds • October 2, 2009 5:08 PM

“Have the proof verifiers been proved correct, and are we sure that proof is correct? If not, then we are entitled to suspect the verifiers might be buggy.”

The thing is, the way computers are written, there are lots of “abstraction boundaries”, between which bugs are a lot less likely than within those boundaries. Your program will very rarely produce the wrong output because of a compiler bug (though it’s not been unknown), and even more rarely produce the wrong output because of a kernel bug. Bugs in compilers and kernels tend to make programs crash.

The way most proof verifiers are written (including the one used here), there’s only a very small amount of code that is required to be trusted to be correct. All the rest of the code simply manipulates the interface exposed by the reliable core, and cannot have bugs that allow incorrect proofs. Since the core is general and simple, bugs in it would tend to show up rather frequently in higher-level mechanisms. So simply by using proof engine a lot, we very thoroughly test the core.

Of course there’s no proof. But you can be extremely confident. Even if there was a proof, we still couldn’t trust that proof absolutely; it would be changing our expectation of any bugs from .000001 to .000000001, which isn’t a significant difference for most practical purposes.

Nothing in the world is certain. Do we know for certain that Perelman’s proof of the Poincare conjecture is correct? It seems very likely, but there’s a very small chance that there’s some mistake in there that hasn’t been caught by anyone reviewing the proof. Do we know, absolutely certainly, that there are an infinite number of primes? The proof can be followed by a grade school student, but can we be absolutely sure? I think that the same things that make us sure about those proofs–being consistent with other mathematics, part of a fabric of coherent theory–make us sure (to a lesser, but still great extent) about the reliability of proof checkers.

“I can write a computable algorithm for testing Goldbach’s Conjecture that either will or will not always terminate.”

I anticipated that objection. Perhaps I should have said, for any algorithm that is known (i.e. can be proved) to always terminate, a program can implement that algorithm that can be proved to terminate. Which doesn’t actually sound all that impressive, now that I think about it. Proving that a program testing the GC would/wouldn’t terminate would subsume proving/disproving the GC. Hmm. I think there must be a way to make my statement stronger, but I can’t think of it.

pdf23ds • October 2, 2009 5:15 PM

Nick,

“are you at all surprised at the skepticism by some comments?”

Not really. I guess I pretty much agree with your comment. I guess I was just making a more limited point about Isabelle itself, rather than the L4 verification project.

pdf23ds • October 2, 2009 5:23 PM

“By definition, algorithms terminate.”

OK, I’m confused here. You’re saying that an “algorithm” that terminates if it disproves the Goldbach conjecture is not an algorithm unless we can disprove the Goldbach conjecture? If such a thing is not an algorithm, what do you call it? Surely “program” is not the best word.

pdf23ds • October 2, 2009 5:48 PM

By “algorithm that terminates if it disproves the GC” I mean one that tests even numbers sequentially until it finds one that doesn’t decompose into two primes, of course.

anonanona • October 2, 2009 5:49 PM

terminal – the end, the extremity
terminate – to bring to the end, i.e., the terminal

So, I guess he means it’s not a real algorithm unless it runs on a real terminal. He is hardcore.

Nick P • October 2, 2009 6:12 PM

@ Dave Walker

Your comments are misleading. I just read the VIPER paper. For one, it wasn’t formally verified. The authors dedicate the entire conclusion to saying their proof was partial, mainly model-checking, and there was no correspondence proof. Second, if you look at its features, it actually is useful. It was just very different and another technology to fall to politics and market forces.

If you want practical processors with formal methods, then you should look at AAMP7G (recent) by Rockwell-Collins and VAMP, which is in the MIPS family. AAMP7G is running separation kernels for safety/security-critical stuff. VAMP is MIPS-like, which might allow us to easily port RTOS’s to it, many supporting MIPS. Also, VAMP supports user/kernel modes and (i think) interrupts. What we need now is formally verified hardware assisted OS and IO virtualization, at least an IOMMU. Then I wouldn’t have to trust those binary blobs. 😉

@ pdf23ds

Your explanation of why we can trust sound provers like HOL was excellent. This same line of reasoning is why most hardware proof effort is aimed at the microcode and a few other specific units. In most cases, if the core works right, the rest is easy to build. Modularity increases overall complexity, but reduces difficulty of verification (any kind). Each component can be proven independently, and then their interactions can be modeled to prove overall system. This is partially why high assurance is moving to separation kernels.

More rigorous math:

verified processor (VAMP/AAMP7G) + verified IOMMU + verified RTOS (INTEGRITY-DO178B/seL4) + medium assurance good middleware (DO-178B networking, USB, Java, etc. stacks maybe?) + modular apps designed to take advantage of it all (perhaps in SPARKS Ada or OCaml/Haskell?) + (simpler) formal proof of their interactions = a system I could trust

Fortunately, all of this exists today. It just has to be properly integrated. Anyone in the know would realize that is a mind-boggling challenge, but I think the rewards will be worth it. At least to those of us who value security, safety and privacy.

pdf23ds • October 2, 2009 6:34 PM

“Your explanation of why we can trust sound provers like HOL was excellent.”

Aww, thanks.

“At least to those of us who value security, safety and privacy.”

Hmm. I’m wondering how you would go about proving privacy. With things like the facebook datamining attack Bruce just wrote about, it seems like that would be a challenge at least several orders of magnitude more difficult than proving the absence of buffer overruns and null pointer dereferencing. What attack models do you account for? Physical access? Direct hard drive platter access? Do you assume access to semi-public data and prove the absence of ways to infer private data?

Would it be possible to design an unkeyloggable keyboard? (I’m sure. I wonder if they exist yet.)

rjh • October 2, 2009 6:38 PM

@pdf23ds:

“You’re saying that an “algorithm” that terminates if it disproves the Goldbach conjecture is not an algorithm unless we can disprove the Goldbach conjecture? If such a thing is not an algorithm, what do you call it? Surely “program” is not the best word.”

A sequence of instructions which terminates only if some property of the inputs holds true is usually called a semialgorithm. There’s some computer science formalisms that define “semialgorithm” more specifically than this, but by and large you can call such problems semialgorithms.

Nick P • October 2, 2009 8:36 PM

@ pdf23ds

It would be challenging to accomplish privacy in general. As you suspected, I’m thinking of specific attack models: protecting private GPG/PGP key; other encryption keys (i.e. truecrypt); defeat keyloggers; prevent screen spoofing (assumed feature of MLS security); anonymous web traffic; network is a black box via effective firewall (red/black separation); private communications over the internet. These are just some of the problems that I’ve been trying to solve in my own designs. Many others are working on them, and most of these are solved. I’ll be specific on one.

You mentioned unkeyloggable keyboard. I think what you want is a trusted path. Many hardware attacks, so the main idea is to prevent remote access software attacks, right? Thanks, again, to microkernels and separation kernels, this has been achieved. A basic design has these components: user application VM (usually Linux); GUI or screen renderer; mouse, keyboard and graphics driver. Only the GUI system can access the drivers, and the VM/apps must go through it. The communication policy of the trusted separation kernel (i.e. seL4), which can’t be overridden, ensures the security of this scheme. The GUI is low complexity (few bugs), gives input only to the partition/VM with focus, labels each window so the source is known, and is the only app with control over the screen (spoofing prevention).

Many defense-oriented OS’s have some sort of trusted path, such as BAE System’s STOP OS (excellent design, btw) and Sun’s Trusted Solaris 8. Their OS’s are so big, though, that they can’t be proven secure. The first good trusted path, imho, was the Nitpicker GUI by Dresden. It runs on their medium assurance L4/Fiasco microkernel. They use it in their Nizza architecture to prevent keylogging and spoofing. Google them and NICTA to see many awesome, practical schemes. Green Hill’s INTEGRITY Workstation also does things this way.

How would this work in practice? I mean, couldn’t the attacker just hack the main VM and disguise the malicious messages or get the key? No. Dresden gives an example of a digital signature for ecommerce. Most functionality would be in the untrusted vm. You’d do most of the order and total it. It would then send the critical shopping data to a small, trusted signing app in a separate partition, running right on the microkernel. You use the trusted path to switch to that app, enter your password to decrypt your signing key, visually verify what you are signing, sign it, and then the signature is sent back to the untrusted side. The secure kernel handles transfers, and the MMU isolates all these processes. I have a password manager scheme that works similarly, protecting my master password and only letting passwords out that I choose.

I hope these examples show why seL4 and the other high assurance separation kernels are so important. Using them, one only has to decompose and structure their app right to maintain confidentiality, integrity or availability. In the eSign app, you have strong assurance of confidentiality, esp. if private key is zeroized after use. In password manager, you have reduced risk. If your firewall sits in dedicated partition in between VM and networking stack, then viral infection or hack of VM can’t disable the firewall. The uses for MILS architecture are many, and what’s great is that it’s actually simple enough for most people to understand. I’ll post or email you links on MILS and usable high assurance products/projects if you request it. Here’s whats relevant to our current discussion.

TU Dresden OS Research and Demo
http://demo.tudos.org/eng_features.html

L4 Family Page (look at Perseus and uSINA)
http://os.inf.tu-dresden.de/L4/use.html

OKL4 Hypercell (commercial, dual-license)
http://www.ok-labs.com/releases/release/open-kernel-labs-new-secure-hypercell-technology-advances-development-of-en

pdf23ds • October 2, 2009 9:50 PM

“Many hardware attacks, so the main idea is to prevent remote access software attacks, right?”

Well, preventing software attacks is certainly important, but what I had in mind was a smart keyboard that would set up some sort of SSL tunnel to the computer and encrypt all of its output so that hardware loggers would be ineffective. I’m not sure how cheaply this could be done, but perhaps would special purpose encryption chips it would be feasible for under $50. Of course, that has little to do with verification.

Interesting comment, though.

Gweihir • October 2, 2009 10:58 PM

So what? Interesting in an academic sort of way but without a lot of practical consequences.

The issue is that they proved the code conforms to its specification. There is a second step that is missing: Proving that the specification describes a “secure” kernel. This is currently beyond humans and machines would need artificial intelligence that not only works, but is incredible powerful.

Nick P • October 3, 2009 12:28 AM

@ pdf23ds

There exists keyboards like you describe. The points of attack become the keyboard circuitry and the software driver that does decryption. Hacking the OS may compromise driver: software exploit defeating hardware security. An alternative scheme would be a dedicated PCI card and keyboard in a Master and Slave situation. Keyboard and card hardcoded w/ private/public key pairs; PCI card sends random session key on boot; decrypts character stream before sending to OS. Most such schemes are vulnerable to power line, tempest, vibration-type and other hardware attacks. As far as keyboard, video and mouse security, I’d only trust TEMPEST-certified, Type 1 products. And not entirely there.

@ Gweihir

In case you didn’t actually read the research before commenting, they did prove that the specification describes a secure kernel. They defined “secure” as guaranteeing isolation between components running on top of the kernel, with communication only happening through the kernel’s controlled, well-studied mechanisms. It’s called MILS architecture. They formulated this in Haskell and Isabelle, then wrote an executable specification in Haskell and Isabelle, connected the two, then wrote C/asm code, and connected the specs to an Isabelle model of the C code. Far from what you suggested, their focus from the beginning was clearly (and formally) defining how the software achieved safety/security goals.

For a better understanding of how this relates to security, look up MILS architecture or the Separation Kernel Protection Profile. Those are the security model. All you have to do is prove a few properties, and then you should be able to write programs that inherit that level of security via careful integration. The best example of a system where “secure” was precisely and mathematically defined before proofs was the INTEGRITY-DO178B Separation Kernel, which was awarded Common Criteria rating of EAL6+/High Robustness during the evaluation. This involved checking architecture, formally proving specs met requirements (SAIC Inc. did that), strong semi-formal argument that code consistent with specs, and extensive pen-testing by NSA.

In other words, one can model what security means for a particular piece of software. We don’t need any magical AI computers or esoteric math. Or a philosophically skeptical view of whether we can ever truly prove anything. We just need a precise and practical definition of security, and that’s exactly what they (and all other high assurance developers have) used.

pdf23ds • October 3, 2009 12:50 AM

“Of course to prove that a program halts does not mean to write a program that determines if the program halts.”

I’m in pretty deep water here, but I understand that (due to the Curry-Howard isomorphism? constructive type theory?) every formal proof corresponds to a computer program. However, the halting problem says that for any program, some provably halting inputs will not be proved to halt. Does this imply that there are some provably halting programs that can’t be proved to halt using the Isabelle proof checker, and others using Coq, and HOL, and so on? Duuude.

Clive Robinson • October 3, 2009 6:55 AM

@ Nick P,

“In other words, one can model what security means for a particular piece of software. We don’t need any magical AI computers or esoteric math. Or a philosophically skeptical view of whether we can ever truly prove anything. We just need a precise and practical definition of security, and that’s exactly what they (and all other high assurance developers have) used.”

Sadly no we need more than “a precise and practical definition of security”. We need a dynamic frame work (think about, known knowns, known unknowns, unknown knowns and unknown unknowns).

Due to unfortunatly being away from home at the moment due to health reasons my access to the Internet is a little limited, so I have not had the chance to go through the specification they used or other supporting information.

However I would be surprised if it considered side channels in any great detail, especially susceptance attacks, of which very very little is currently in the public domain (although I have been banging on about it for many years).

The simple fact is that a secure system is “fighting the last war” actively and looking passivly for “oddities” that might or might not be a new war or prelude to one…

What is needed is a secure framework where each “user module” within it (both hardware and software) does not need to be designed securely just optimaly.

That is each user module is effectivly jailed by the frame work and the resourses it has access to are strictly controled by the framework under the guidence of a security hyporvisor that is driven from security rules system (which is the tough bit). The framework and hyporvisor are designed so that anomalies are detected and “limited” or “stoped” untill the security rules system certifies the anomalous behaviour.

Yes this means that the framework is both a hardware and software system.

As part of the framework a “security/forensic savant” is required that can freeze and copy the current state of a user module and any communications to/from it, automaticaly without the sandbox becoming aware that it monitoring is in progress (yup a seemingly very difficult problem).

We are starting to see the early stages of such frameworks however the ones I have looked at do not appear to recognise side channels in any meaningfull way.

I would hazzard from what has been said on this blog page that the OS under discussion would be capable of forming one part of a user module, and augmented to provide part of a framework.

As I noted earlier it is not possible to have a 100% secure system but you can certainly via a security ECC system constrain what goes on to limite the potential bandwidth of a side channel etc to an attacker (or ordinary user 😉

The real issue with security currently is “efficiency” or “bang for your buck”, as long as performance specmanship is the marketing tool of choice systems will probably never be secure…

Section9-Bateau • October 3, 2009 6:56 AM

“for the first time a team had been able to prove with mathematical rigour that an operating-system kernel—the code at the heart of any computer or microprocessor—was 100 per cent bug-free and therefore immune to crashes and failures.”

This has been done before, probably somewhere between a half dozen and a dozen times. It is rare, but several projects come to mind off the top of my head (Blacker, GEMSOS, Cainware(as much as I’ve heard that is bad about it’s development), and others that their names are not even public.

Of course, most of these are “in the context of non-malicious, normally operating hardware” but still, we assume that with everything we deal with on a daily basis.

I’m sure I’ll have more comments, but just reading the first bit here was enough I had to get this fact in.

Clive Robinson • October 3, 2009 1:59 PM

@ pdf23ds,

“what I had in mind was a smart keyboard that would set up some sort of SSL tunnel to the computer and encrypt all of its output so that hardware loggers would be ineffective.”

That would be easy enough to do but actually not that usefull these days.

The problem is “end runs” around any security measure you put in place.

All security is about access to an object be it physical or informational.

In essence the access is a form of communication and Shannon had a reasonably good model for a point to point communications path.

However it ignored the problem of the end points, by assuming they where not in the attack model. Unfortunatly they cannot be secured unless they are part of the secure communications path…

With an IO device like a keyboard at some point a secure path ends and it is at this point it becomes vulnerable to plain text snooping (microphone, camera etc etc).

If you think about it the sound of your fingers pressing the keys is just one of a number of attack points you cannot easily defend against unless you yourself and the keyboard are in a secure environment (TEMPEST Cell/vault etc).

Likewise at the other end of the communications path you have to get the keypress information into the application, and in turn the application will normally give you feedback of which key has been pressed.

An attacker can intercept the “plain text” to the application (unless the app takes in keyboard cipher text directly) or from the application to you via the feedback path.

Then there is another problem on the secure comms path which is lack of entropy…

Unless the keyboard encryption takes into account this issue the result will be a simple substitution cipher on each key pressed…

Hey ho life is never easy when it comes to security even for the simplest of things 8(

Clive Robinson • October 3, 2009 2:26 PM

@ pdf23ds,

“Hmm. I’m wondering how you would go about proving privacy.”

If you think of it falling on a scale from zero privacy to full privacy the end points are relativly easy to prove in terms of access.

However except for the end points (full / no access) I don’t think you can.

Partial privacy is about controled disclosure and is an altogether more complex problem.

Not only has it to do with primary access control but also about continuing access control by preventing duplication and disclosure by the entity given primary access to third parties or use for anything other than the autherised use.

In essence it’s the flip side of DRM…

pdf23ds • October 3, 2009 3:09 PM

“The problem is “end runs” around any security measure you put in place.”

Right, I didn’t mean to deny any of that. It doesn’t necessarily mean that SSL keyboards wouldn’t be worth it.

“Then there is another problem on the secure comms path which is lack of entropy…”

Would that actually be a problem with an actual SSL tunnel? I thought the encryption used there was pretty good. Of course, there would be a big danger of having some proprietary, “our programmers couldn’t crack it” protocol whose only purpose is to give flimsy cover for marketing claims.

Nick P • October 3, 2009 10:39 PM

@ Clive Robinson

No doubt we need an architecture like that, but we have all tried and failed. Probably far off, and market forces will fight all progress unless OEM’s sign on. I’m not trying to say the MILS architecture is perfect: it’s just incredibly useful, easy for developers to understand, and in past few years a ton of RTOS’s, virtualization schemes and middleware have appeared for it. In other words, until we have that perfect dynamic security scheme, MILS is the best holdover for many problems.

As for side channels, I’m almost sure they weren’t covered. The separation kernel is about software, not hardware, security. The SKPP-compliant kernels address covert channels, but they do it by a fixed processor allocation scheme. That’s unrealistic. In my S.K. designs, I use fixed space partitioning but dynamic time. Covert and side channels still an issue.

@ pdf23ds

Read Clive’s post again. He basically said what I said, but gave more specifics about threats. Take the camera threat, in particular, very seriously. You beat a $80 keylogger and they just install a $100 color wireless microcamera. I’ve done it, and I was a rank amateur then. Many physical attacks. Your better off using a transparent keyboard and computer, and physically examining it before use if ur worried. That’s what I do when the stakes are high. 😉

Nick P • October 3, 2009 10:56 PM

@Section 9-Bateau:

It would appear that this is a repeat, but its not. Systems like GEMSOS aim for A1/EAL7, which is weaker: the requirements and design must correspond formally, but not the design and the code. The proof chain stops before you get to the code, and semi-formal “arguments” and testing are used instead. That’s actually worse than BSD, which has many eyes and years of experience ironing out the bugs. Additionally, the results for most other A1/EAL5-7 products were never made public: no peer review of code for bugs. This is the first time this level of verification has been performed on a non-trivial operating system, and the source will be released. Next they will verify the assembler.

You are right about the hardware assumption. Fortunately, the separation kernels need minimal hardware. Mainly the CPU, MMU, Northbridge and RAM. The rest can crap out and the OS will still be fine, but useless. It’s the services layered on top of it, like device drivers and file systems, that will need reliable hardware. The cool thing about MILS is that the TCB for each partition is different: only what’s necessary (or in kernel mode) is included. So, even with the hardware assumptions, we still have a very high assurance kernel. When coupled with quality hardware and a high availability solution, the hardware assumptions are even more of a safe bet.

Nick P • October 3, 2009 10:57 PM

@ Clive Robinson

Btw, sorry to hear about your health. Seems like its been going on for a while now. Best wishes to you for recovery.

Clive Robinson • October 4, 2009 8:04 AM

@ Nick P,

“In other words, until we have that perfect dynamic security scheme, MILS is the best holdover for many problems.”

I’ve just remembered we’ve had this conversation befor when talking about IO security 8)

I like MILS for many reasons, as you say it’s not perfect but then I doubt that anything ever will be 8(

However one nice feature is it is modular and as such would co-exist quite comfortably into the sort of framework I was discussing.

The downside (apart from side channels) is it does not quite go far enough in seperating applications from security.

My (somewhat quaint) view is that a framework should be such that the unix “small tools to do big jobs” “pipeline” philosophy would be extended. Such that the tools could be written without security being a consideration.

Application development would be split into the three logical parts of User interface / application specific logic / extended OS functionality. That is the User interface carries on going the way of web development, application logic the way of “5th gen scripting of tools” and the likes of DB engines and other mainline back end services become part of the OS interface.

Oh and the business about Error Checking Corrrection (ECC) systems. It is inefficient (but who cares 😉 but NASA and the like use voting systems for reliability. What few people have voiced (but I hope have thought about) is applying the same philosophy to security.

That is three different teams build the application logic using different scripting languages, when run in parrelel the three systems should agree with each other on what is to be done. If they differ you have a problem in the specification or implementation either of which is a security risk and needs to be resolved.

The important issue is that security is and probably always will be a moving target. Even security practitioners have difficulty keeping up with it, you cannot expect jobbing programers to even remotly get close.

Therfore you have to remove the security asspects away from what they do and let them get on with what they are good at and let the security proffesionals get on with what they are good at.

Splitting things up the way I have suggested in the framework is currently the best way I can think to do it.

However ther is one proviso those “pesky programmers” will have to pull their socks up with regards error and exception handeling, which most code cutters are sadly deficient at currently 8(

A modularised development must have a proper exception handeling system to work effectivly. It would provide not just a major improvment in security but fault tolerant systems in general (but that’s another “beef” for another day 😉

Clive Robinson • October 4, 2009 8:49 AM

@ pdf23ds,

“Would that actually be a problem with an actual SSL tunnel? I thought the encryption used there was pretty good.”

It is improving but it’s not perfect (but hey I and most other people had to learn by experiance 😉

One issue of all encryption systems is low entropy and what effectivly becomes code book encryption.

If you have only 96 keys then no matter how many bits in your key or block cipher you end up with 96 substitutions…

However the simple (and incorect) way to deal with this is either to use a stream cipher or a simple chaining block cipher.

Both of these have problems with synchronisation and authentication and for various reasons have other security faults.

There are ways to do it but…

Do you remember the problems with WEP…

There are subtalties that can get the best of us into trouble.

Oh and then there is traffic flow analysis to deal with this adds a whole host of other problems ontop of things.

And these are just some of the “publicaly known” problems.

On top of this there are side / covert channel issues.

One of which is hardware manufactures using spread spectrum techneiques to beat EMC masks rather than to reduce what is eminating.
A knowledgable attacker will know the spreading sequence used and just despread to get the original signal back…

This has all sorts of advantages to the attacker as it enables you to pull out just one device hiding in amongst many…

Then there are little EmSec tricks like using low level RF carriers to illuminate a target device and get it cross modulated with things that are going on inside the target.

Oh and then there are suceptance attacks which I’m absolutly sure we will hear a lot more about in the future.

They are a form of “fault injection” attack, you inject “energy” into the target via some form of carrier (power supply, RF, sound etc). You modulate this carrier with your chosen attack waveform. Surprisingly this form of attack can work it’s way very deep into the hardware logic, thus geting you past the “clocking the inputs and outputs” method of limiting side / covert channels.

If you can find the correct waveform and a method of syncing it up it is theoreticaly (and practicaly) possible to alter the internal logic state in a predictable way so causing software to make incorect branches etc…

And there are a few other tricks to follow after that I can think of as well 8(

So you can see why some of our more security concious friends like vaults to work in 😉

Thunderbird • October 4, 2009 1:31 PM

Clive Robinson: “However I would be surprised if it considered side channels in any great detail, especially susceptance attacks, of which very very little is currently in the public domain (although I have been banging on about it for many years).”

Since I don’t find anything (except this blog) when I search for “susceptance attack,” I guess there is very little in the public domain. What is a “susceptance attack,” if you don’t mind saying?

Nick P • October 4, 2009 1:41 PM

@ Clive

Yes, we did have this discussion. And separating interfaces and security-critical code was part of it. Fortunately, MILS was specifically designed for this. The idea is that you certify one module, then modules that depend on it, then modules that depend on it. It’s like chaining a bunch of black boxes together, which (like you wanted) let’s developers focus more on their job than security. This contrasts with the [unevaluatable] monolithic approach.

Personally, I don’t think side channel attacks will be a big issue here. I know I’ll draw some heat on that, but most of the easy attacks facing average users are software-related: malware; spoofing for phishing; botnets in DDOS. MILS and certified middleware can be (and has been) used to defeat these threats. And if we’re worried about emanation security, we can do what I suggested before: just stay on the move with an energy-efficient laptop. Pull the batteries out and put the system in a safe when not in use. I’ve recently been toying with ways to secure the BIOS and bootcode. That issue must be resolved, imho.

Nick P • October 4, 2009 4:10 PM

What Clive describes is usually referred to as TEMPEST, side channel attacks or emanation security (EMSEC). On most unofficial web sites, all the information is usually clumped together under one of those names. Clive is just using the proper terminology… yet another reason to expect he is or was an “insider.” We’re onto you Clive… 😛

If you want more information on it, you can start with the resources below. From my limited understanding, his susceptance attack means RF waves are injected into the device or wire in a certain way. Then, measurements are made of any resulting RF activity. Attackers analyze the results to see if any information leaked. This effect can be accidental too. Cell phones constantly emanate EM waves that, when mixed with devices, can cause leaks of confidential information. As an example, cell phones (one model/carrier in particular) weren’t allowed within 10-30 ft. of a STU-III secure telephone because the cellular transmission caused the STU circuitry to leak the secret keys as RF radiation. The manual I read said that if someone with a cellphone, talking or not, walked near a STU-III, then it was considered compromised. Injection attacks are very powerful. Note: I think these attacks are actually under the codeword TEAPOT rather than TEMPEST. Search words like TEAPOT and NONSTOP combined with words like TEMPEST, emanation, etc. Better results.

Sadly, I seem to have lost most of my EMSEC bookmarks a few restores ago. Good news is I remember some of the sites with the most info. Just dig through these as much as you like.

Complete Unofficial TEMPEST page (best starting place)
http://www.eskimo.com/~joelm/tempest.html
Note: Is currently down. Check the Wayback Machine. Archive it yourself if possible. Best non-secret info source.

Books I’m Looking Into Getting To Improve EMSEC(Clive, what do you think about these?)
– Architectural Electromagnetic Shielding Handbook by Hemming
– Design of Shielded Enclosures by Gnecco, Certified TEMPEST Professional

Some Declassified TEMPEST Docs
– http://cryptome.org/nt1-92-1-5.htm

An example of TEMPEST products
– http://www.cryptek.com/products/emanation_security_products/

NSA’s List of Level 1 Certified Products (where I shop 😉
http://www.nsa.gov/applications/ia/tempest/Level1Certified.cfm
Note: If you use NoScript, you will have to hit “allow nsa.gov”. Allow them to run scripts on your machine at your own risk… hehe

Google Books Injection Probe Example
http://books.google.com/books?id=MuxJXKuHIpAC&pg=PA461&lpg=PA461&dq=%22injection+probe%22+attack&source=bl&ots=E3BzXTfV_h&sig=W6muyQoEneg1CV7K_TFiQebqe1s&hl=en&ei=1wbJSqyVLKSStgeHkPjtDg&sa=X&oi=book_result&ct=result&resnum=3#v=onepage&q=%22injection%20probe%22%20attack&f=false

Clive Robinson • October 5, 2009 1:15 AM

@ Thunderbird, Nick P,

If you have a machine be it purely electronic or electromechanical or even just mechanical and you put it in a nicely controled RF field, it’s working will cause the field to be modulated by it’s workings.

This by the way works not just with metal but anything where it’s dielectric constant is sufficiently different from what surrounds it (so wood and plastic will effect some frequencies)

You are used to the idea of this interferance to an EM field with for instance X-Rays, Offset Radar, and more recently millimetric body scanners. You also get the same effect when you drive down a road under bridges etc and your VHF station flutters.

Oh and of course your eyes we see by reflection and transmission, although our eyes are not designed to see phase modulation and are fairly insensitive to amplitude modulation above a couple of Hz in the center of our visual field.

A clasic visable effect is looking at moonlight off of lightly disturbed water such as the sea or a lake we see light twinkle as light waves add and subtract by comming into and out of phase by different path lengths.

Now think of those funny looking helix cowles ontop of “foul air” pipes where the wind causes them to spin and in the process causes the presure to drop in the pipe. When new they are often quite shiny and when turning slowly we can acuratly tell the speed of rotation either by reflection or transmission of light…

That is we can get usefull information on this simple mechanical system just by observing what it does to a surounding EM field…

One of the things we are going to hear more about is the effect wind turbines will have on TV pictures if we all start putting them up on our houses…

What is less commonly known although it should be obvious from basic physics lessons is that a current in a wire also modulates an EM field around it.

When not being used for EmSec or TEMPEST engineers refer to the effect as cross modulation, and it is generally considered a real pain to deal with for EMC testing.

Also it can be a real pain due to mechanical vibration on such things as coils and physical tuned circuits such as slots and cavities and even antenas.

However when used for EmSec / TEMPEST it has a variety of names (some of which Nick P mentioned).

However although using an EM or other energy source (remember mechanical sources such as sound 😉 directed at the target these are effectivly “passive” attacks. That is they do not usually effect the target equipment…

A suceptance attack however is used to “inject faults” into the target equipment.

That is you use your energy source at a high enough level such that it effects the way the equipment works.

This works with any kind of amplifier a classic example is leaving your GSM cell phone on near an audio amplifier that is not properly screened. You hear the “envolope” of the digital transmission in the speakers as a sort of rasping noise.

Now you have to apreciate that digital electronics is still analog electronics but with a lot of gain…

An example of this is with CMOS logic (old 4000 series) where you have an inverter (NOT NAND NOR XOR) and you connect a resistor from the output back to the input. It acts as an analog amplifier.

In the early days this trick was used for all sorts of clever tricks by engineers but it has mainly fallen by the wayside and the only place you commonly see it is with XTAL oscilators.

It even works with some TTL gates (74 series). If you wire up a Schmitt inverter as an XTAL osc running at 30MHz and capacitivly couple an audio signal into the input, this fractionaly changes the bias point of the gate input with the result the 30MHz signal gets sufficiently phase modulated that the third harmonic can be clearly heard on an FM radio. And thus you can use it as a low power FM transmitter or bug (a design for one using exactly this trick was published in an early electronics magazine around 1977)…

Now imagine what happens with a low power VHF transmitter and a PCB which is not properly screened…

It was not unknown back in the 70s/80s for microprocessor systems to fail when a security guard etc fired up their two way radio in or around a computer room. Or for VDU’s (any one else remember them) to have their screens break up or show odd charecters. If you read Clifford Stoll’s book about tracking down a german cracker he mentions “line noise” and simulating it by jangaling keys across the terminals of a break out block. It worked because back then what we now call EMC was a very real and anoying problem holding back the electronics industry.

That is all digital circuits are “susceptable” to interferance from energy fields if the proper steps are not taken.

Now imagine if you will an important item of security equipment a True Random Number Generator or TRNG. What would happen if you say subjected it to an EM field?

Well you can now read up on it as a couple of researchers at Cambridge Labs (UK) have recently presented a paper where they show the entropy went from 32bits down to 8bits. With just such a simple attack.

Now imagine if you will that by using a number of different EM frequencies you could target diferent parts of a circuit (you can due to track length issues). And that these EM fields where either pulse or phase modulated with an appropriate pattern?

It would be the same as directly injecting a signal onto an input gate as in the TTL FM bug above.

That is you could inject a “fault signal” of your own chosing into various parts of a “black box” system you wish to attack.

Now to make it realy usefull further imagine that by listening in to a different EM signal you could get information out that you could use to syncronise your “fault injection” waveform.

You potentialy have a way to effect the operation of the device you want to attack to make it do what you want it to do…

And yes these attacks do work I found ways to effect the Mondex electronic wallet and a hand held gambaling game to what would have been my advantage (if I’d been dishonest) back in the 1980s.

Now the cat is “officialy” out of the bag as far as accademics are concerned with the Cambridge Labs paper I expect there to be a whole bunch of other researchers jumping onto it.

That being said I did tell Ross Anderson many years ago about it when he was trying to find ways around DPA using unsyncronised logic.

If you want to know more have a hunt around for “injection locking” for such things as PAL/NTSC colour sub carrier syncronisation, PLL threahold extension, carrier resyncronisation in data coms and various forms of Spread Spectrum systems. Ian Hickman of Wireless World wrote a couple of articals on injection locking and practical experiments.

Also look up “parametric amplifiers” to see another exploitable effect.

The important thing to remember is these EM fields used for susceptance attacks do an “end run” around most EMC / TEMPEST / EmSec bandwidth limiting filters…

Pragmatist • October 5, 2009 8:40 AM

Now all they need to do is get a computer chip that is proven to work correctly to run it on.

Oh wait, they don’t have those?

Nick P • October 7, 2009 6:31 PM

@ Pragmatist

Actually, they do. I mentioned a few in my post. You can build your own out of simpler chips (see Magic1), which are easier for COTS vendors to get right. In addition, there are a few partially or fully verified designs: VIPER, VAMP, AAMP5, AAMP7G. You could also take an open core/spec, like OpenRISC or SPARC T1/T2, and reimplement it using a high assurance methodology with extreme testing.

In other words, nearly bug free processors are very possible. The market just doesn’t seem to want them. Only safety-critical or security-critical markets even consider it, and most of them are satisfied with a ARM chip from a good manufacturer. Unless you want to get one of the aforementioned designs, and run it on a high quality ASIC or FPGA, you will have to settle for a typical processor. 🙁

Nick P • October 7, 2009 6:37 PM

@ Clive Robinson

I appreciate your reply. Since I do software red/black vpn/firewall designs, that Cambrige research was particularly interesting. I was checking out cambrige just a week ago. I don’t know how I missed it. Thanks for the tip. 😉

Information about EMSEC is particularly hard to come by. One must solidly grasp many technical concepts related to EMF to put all the pieces together that are public. Those that don’t have access to more readable information that isn’t public. You never cease to amaze me with your knowledge on the subject. It leads me to believe that you are or were… well, you know where this is going. 😉 Funny thing is I actually keep a copy of each post you make on it for future reference.

I’m mainly a software & systems guy, but I’ve recently been trying to branch out into secure hardware. Do you know any good publicly-available books on the subject? Something a somewhat technical, but not EE major, could understand and use to add at least a little EMSEC to their designs. If you’ve seen any you liked that are on Amazon or whatnot, I’d love to read up on it more.

Clive Robinson • October 8, 2009 12:21 AM

@ Nick P,

“Information about EMSEC is particularly hard to come by”

It is and it isn’t as you note a lot of the information is out there just not in an EmSec format.

However that may well change soon thanks to Russia effectively mandating TEMPEST type requirments on general use systems (not sure which will be quicker learning Russian or awaiting english translations 😉

EmSec / TEMPEST is an engineering subject where practical methods are driven by complexity. Not just of theoretical ideas but also due to interactions of all the components involved.

Thus it tends to be “rules driven” for design and likewise for certification, and the rules generaly suffer from “over kill” for good reason (ie a large amount of safety margin).

Actual testing can look like “witch craft” but in essence is quite simple.

Basicaly you have a “black box” system that has a number of ports through which energy can be transported.

The trick is to identify all th ports and all the energy.

The important thing to remember is that with energy “what goes in must come out”, but in maybe a different form…

For instance a simple device such as a loud speaker you have electrical energy in and sound, E fields, H fields, heat, etc coming out (emission).

But… the loud speaker like any transducer is a two way device sound energy in will produce electrical energy out (suceptance).

Unfortunatly all methods of transporting energy are “inefficient” and the “transmission loss” indirectly tells you they are transducers in their own right…

The trick with EmSec is ensuring that the energy coming out is in a form where it is not carrying “information” that would be of use to others.

Ultimately all energy ends up as back ground heat in a closed system due to entropy (moving from an organised to a disorganised state).

Without going into details the back ground heat is also “noise”, all physical items act as transducers and convert heat into an equivalent “thermal noise” (and vice versa). Thus at any given temprature there is a certain degree of background “thermal noise”.

Now “information” implies a “signal” and signals have certain charecteristics. One of which is bandwidth another is energy, and importantly a transmission medium to carry it.

If you limit any one of the three sufficiently then the “information” is not going anywhere but the energy has to…

The first idea of TEMPEST was to reduce the energy of the information signal below the back ground thermal noise (also called the noise floor).

Thermal noise is however a signal in it’s own right and therefor has bandwidth considerations, thus the wider the bandwidth the more thermal noise energy there is (as it is actually many independent signals the average goes up as the RMS of them all).

Thus at any given bandwidth you would expect an “average” thermal noise level. Which is where the -174dBm (in a 1 Hz bandwidth) you sometimes see quoted comes from.

The usuall way of limiting bandwidth is with filters.

However most engineers do not think of what a filter actually does.

By limiting the bandwidth the excess energy has to go somewhere and as most filters are made only of “reactive components” the net result is it gets reflected back towards the source.

One of the problems with this reflected energy is that it can without proper precautions end up on the “common ground” of the equipment.

The important weasle word is “common” which means that the energy can get back into any part of the black box contents via this common path…

Therefor it is better to use other types of filter that contain non reactive components that “disipate” the reflected energy as “heat”. Such filters also need to be designed to limit the ingress of energy and preferably divert it away to a suitable disapating component.

However all physical components have dimensions which has a side effect of making them reactive components which will radiate or pick up energy.

Thus components can “cross couple” energy to each other and bypass filtering components or get from one independent / isolated circuit to another.

To prevent this physical partitions are placed between components that have desirable charecteristics to reduce the type of energy being coupled from component to component.

Often designers will concentrate on one cross coupling effect and forget (or not know) about others.

Thus “rules of thumb” develop one of which is about cable seperation of 1meter between “red and green” or “red and black” cables (or plaintext circuits and cipher text circuits).

Obviously these “rules of thumb” have significant effects on the resources required to make equipment.

However two general rules apply at all times,

1, Reduce the energy.
2, Reduce the bandwidth.

A lot of this aspect of EmSec can be found in practical guides to Electromagnetic Compatability (EMC).

However be warned that some “low resource” EMC solutions make EmSec problems considerably worse.

One such trick is to realise that the EMC limit masks are “wide band” and that most EMC “problem signals” are have a “narrow bandwidth” so spread spectrum techneiques are used to widen the signals bandwidth and thus lower it’s level to get below the mask.

This techneique although effective to get below an EMC mask is not resolving the EmSec issue of “radiated energy”. It is still being radiated and thus a “deconvolving receiver” can remove the effects of the spreading and get the original signal back.

But worse the process is syncronus to the EmSec target, which means that it helps reduce other non corelated signals. Thus lifting the target out of artificialy generated noise by other similar equipment.

Thus making,

“a single tree deep within clearly visable outside the forest, as though standing on a grassy knowl”.

There is a lot lot more to EmSec but knowing the fundementals in a practical view point will take you a lot further than the “rules of thumb” will.

Another good source of information is the ARRL and RSGB guides to equipment design / construction and antennas for amature radio enthusiasts.

However that as the say is but the first steps along the pathway.

Early TEMPEST did not consider “side channels” such as time based attacks.

There is a story about a tape based OTP system that unfortunatly had hold and release timing problems in the relays doing the XOR function. Thus it was possible to see which bits had been flipped and those that had not and thus get the plain text back…

This apparently gave rise to the notion of using additional relays to “re-clock” the output.

The more modern computer idea (for different reasons) is “pipelining”.

Thus another rule,

3, Clock your inputs and outputs.

Which limits the effects of timing jitter.

As you get to see more of these rules you start to get the feeling that you have two things working against you,

1, Complexity.
2, Efficiency.

Both of these give rise to the majority of side channels that you will see in comercial equipment.

And the key to both is managment by effective design methodology. Which usually boils down to modularity where each module does one and only one job, and is effectivly segregated from the others via an effective framework.

As some say EmSec “ain’t rocket science” whilst forgeting to add the rider of “because that’s to easy” in comparison…

SCP • October 15, 2009 2:29 PM

For those generally interested in Program Proof you may wish to track down details of the Tokeneer project. This was formally specified (Z I believe), written in SPARK Ada, and proven (at the Ada level) to be compliant with its specification and free of specific classes of errors. There should be links to it from http://www.sparkada.com.

There also seems to be an awful lot of misdirection on proving program termination. Those interested in high assurance programs typically avoid constructs that are difficult/impossible to analyze. For a usefully large set of programs it is possible to analyze them to assure they complete as required Have a look at http://www.absint.com.

There are still issues around, but the use of ‘formal methods’ and ‘program proof’ is providing a useful and practical means of engineering high-assurance software.

D • October 24, 2009 11:53 AM

haha “assuming no increased complexity from the increased complexity…” that gave me a great smile and chuckle with my morning cup of joe, thanks for the post!!

MOHSIN • August 30, 2010 12:11 PM

Prove that the program segment

y:=1
z:=x+y
is correct with respect to the initial assertion x=0 and the final assertion z=1

THIS IS MY QUESTION,PLEASE SOLVE IT AND REPLY IMMEDIATELY

Leave a comment

Login

Allowed HTML <a href="URL"> • <em> <cite> <i> • <strong> <b> • <sub> <sup> • <ul> <ol> <li> • <blockquote> <pre> Markdown Extra syntax via https://michelf.ca/projects/php-markdown/extra/

Sidebar photo of Bruce Schneier by Joe MacInnis.