Theorem Proving
There is quite a bit of that technology used in industry. Extensive theorem-proving scaffolding and refactoring to manage security relationships has been applied to the Windows kernel in the last few years.
Aussie boffins have developed an operating system micro-kernel mathematically established as free of many types of errors. The development points the road toward "safety-critical software of unprecedented levels of reliability" for applications such as aircraft and cars. The software - called the secure embedded L4 (seL4) …
...to computers coding and debugging by themselves. We already have self modifying code, of sorts. A few more years and we'll only have to ask the computer what sort of program we want, or behaviour desired.
"Today the Government announced that it had successfully completed the migration of all civil and military operations to the latest generation of server operating environment, programmed with the input of just 3 simple rules...."
Let me get this straight: they developed a mathematically correct kernel by analyzing C code, and then wrote the final kernel in C.
I trust I'm not the only one who sees a flaw with this....?
Will their product be part of the Obfuscated C contest? Under the "mathematically correct" category?
are the bonking mad ? That language is flawed by design ... There is a reason it is called 'c' : that was the final grade it got when they handed it in ...
have they tried analysing the bartender problem with that tool of theirs ?
for people that don't know the bartender problem : 3 men walk in to a bar. and order a beverage,
Beverage costs 10 pence. the bartender receives 30 pence. The innkeeper says : these are good customers give them a pence discount on their tab.
the bartender can't split the 5 pence. so he gives each customer 1 penny back and keeps 2 for himself.
from the customers perspective : they only paid 9 pence each.. 3x9 = 27 , add the two pence the bartender kept. total : 29 pence... where o where did the thirtied one go ...
Unfortunately a mathematical proof of correctness may prove that some set of known types of bugs don't exist and it may prove that the program actually matches the specification. What it doesn't prove is that the program is what the customer wanted (i.e. the specification is never complete and will change over time so insisting on it being complete and static is a very good way to get a disappointed customer).
Does proof of correctness result in code that is optimally able to be maintained (oops, sorry - if it starts out life correct then it never needs maintenance does it?).
More importantly, our happy user needs to use this kernel to do some real work so they install a web server on it, along with php, then hire a cheap programmer that has read a book on PHP to write applications for it.
The eventual end user knows nothing about any of this and compromises the integrity of the system by writing down passwords on sticky pieces of paper or surfing pr0n sites that use have bonus cross site request forgeries embedded in them....
It may be nice to have a more robust Kernel but I think the money would be better spent on researching how to fix the real problems that plague computer systems.
As I remember it, all you had to do was give him two contradictory orders at once at the same level of priority and he'd undergo a massive psychotic breakdown.... Using the Cretan paradox in one form or another to make a computer overload and blow up is the oldest trick in the sci-fi book.
Similarly, in the context of this story, the fact that they've mathematically proved it to be formally correct really just means that now they're half-way to proving the overall formal system's Gödel statement, and thereby demonstrating that it is either incomplete or inconsistent. Well done them! I look forward to the inevitable future moment when this proven-mathematically-correct system goes completely haywire and starts spewing out random garbage!
So, a team of clever people, over years, has recreated a light version of secure BSD *nix.
But, mathematically proven, like the heavier than air machine cant fly, radio coils must be over a specific (big) size...
Now we start checking the hardware BIOS, silicon logic in the CPU and eventually the firmware in the attached devices.
Paris, because even she knows when enough is enough, sort of.
The current by-line on the front page is "Computer scientists claim to have built a Linux kernel for embedded...", but nothing here says anything about it being Linux related; indeed, it's a microkernel. It could possible run linux inside the proven correct microkernel, but let's not confuse the issue.
Maybe it's just me, because I'm not usually the first to think of these sorts of things, but...
Isn't the idea of a formally proven kernel written in C nothing more than an academic exercise without a formally proven C compiler?
Not to mention the CPU and chipset as well, while we're at it.
@The Other Steve: Nice one, Dijkstra on the other hand got angry when you suggested testing something he had proved.
@Brian Miller: Not a flaw at all. It is possible to write secure C, just as it is possible to write secure assembly (after all, any secure code must be secure machine code at the final crunch). So long as you have a secure C compiler (mathematically correct) you are OK. Exactly because C is so small, as a language, it is less hard to prove correct.
IIRC VIPER hit trouble due to the team assuming the implementation tools (turning the absctract register based machine desing into actual gates on chip) had no errors in them. This was incorrect. When the design had demonstrated bugs the project hit the skids.
Lesson. You need to verify the *whole* toolchain. Just because *most* users of the (commercial) design tools have no problems does not make them problem free.
Going from memory (V. old Byte article early 80s) The architecture was basically a 16 bit 6502. The 1st implementation was a gate array using a series of finite state machines using a 26Mhz clock to get 1MIPS. I seem to recall some fairly simple changes upped the speed quite a lot but made the verification harder (verification being the actual project focus)
I think RSRE had a buy British policy so when to their chums at GEC for that stuff. Who knows what would have happened if they had used VLIS logic instead (company that fabbed the ARM series).?
I suppose the proof starts of a bit like this:
Suppose there is ...
and then goes on to use base assumptions to mirror physical events controlled by the kernel.
Which is ok, fine and dandy - it really is a brilliant start but kernels tend to operate with voltage changes effected at very high frequencies yes?
So there will always be a physical element that the proof cannot completely cater for?
So, good model = good proof.
The article mentions C, but that is known to have several internal contradictions and *that* would make a mathematical proof impossible. However, one could (with some effort) go through all those inconsistencies and resolve them one way or the other and end up with a C-like language that was well-defined, and then use *that* to produce a kernel that was proven. That would be a useful exercise if it yielded new techniques. (I don't want to mock, too much.)
For example, you might write a compiler for the new language. Of course, then you'd need to prove the compiler. And you'd only be able to run the compiler on a proven operating system, which you don't have yet. And you'd only be able to run either on proven hardware, which I suspect also that you don't have yet. (OK, just a little.)
But all that is for a *mathematical* interpretation of "proven correct", which is a boolean attribute, whereas engineers recognise a continuum of...
Proven wrong
Smells bad
Compiles, but I haven't tried it out yet.
I'm quite proud of this and willing to publish it.
I'm quite proud of the test suite, and willing to publish that too.
I'm quite proud of the original requirements spec, and willing to publish even that.
I have professional indemnity insurance that covers this.
(That's not mockery by the way. Outside of the maths department, no-one ever *proves* anything, but people sometimes put their money where their mouth is and you can tell a lot by just how much money they, or more accurately their insurance companies, put up.)
"All this heavy mathematical lifting means that the kernel ought to be immune to common types of attack, such as buffer overflows."
And the first half hearted assault which results in a buffer overflow will render their testing model fundamentally flawed and their promises just so much hot air/commercial posturing/spin?
He might have fooled you into thinking 1=2 but he didn't prove it mathematically - its the same technique used by city types to prove they're useful. Works on politicians but not reality.
@Don Mitchell - you need to apply it to the whole 'kernel' to be of any use, and then be prepared to fix the system when you find problems - but as that would stop a lot of it functioning usefully....
Whilst I'd love to stand up and wave the flag for Linux, I get a bit worried whenever a boffin stands up and says something is "mathematically proven". Maths is just modelling tools that allow us to describe real world events in a manner some can understand, and often include plenty of assumptions. Of course, if your mathematical model is flawed or just wrong, then you get some fun scientific gaffes such as the so-called proof that bumblebees can't fly. Actually, if you use the standard aerodynamic models the maths says they can't, but if you use the special models for helicopter flight then it all looks much better for our fuzzy friends. It's probably a good thing bumblebees put a lot more faith in empirical testing rather than mathematical theorems, and so do I - until it is thoroughly tested in a real environment, nothing is proven.
@Suburban Inmate
The proof are being done with Isabelle, which is an "interactive theorem prover". Essentially this means that the computer is doing the number crunching and humans are directing the proofs and doing the clever stuff.
@Anonymous Coward
The main problem there was folks making overly bold claims. The proofs themselves were valid, just not as far reaching as some thought. Things have progressed since then but there are still boundaries with every formal verification.
@Brian Miller
Your comment makes no sense. They used a theorem prover, called Isabelle, which is written in Standard ML. This supports doing proofs in higher-order logic (a formal mathematical logic). They used this logic to model the semantics of C code. This semantics is then used to verify correctness properties for the source code of the Kernel.
@Apocalypse Later
This is the entire point of using an interactive theorem prover. It should guarantee that there are no holes in your proofs. The main problem is making sure you've proved exactly the right thing i.e. that your models are right and that they are detailed enough.
This post has been deleted by its author
Remember this old logos: In theory, theory and practice are the same, but in practice they are not.
If you work in this game long enough you realise that a real-world OS running on real-world hardware is not deterministic. The theory says that it is and if everything runs well, it is; but nothing runs well all the time and, alas inevitably, red faces all round when lots of great mathematics go up in a puff of "alpha particle induced memory error" smoke (or something similar).
Cast back to LTCM Ltd. and the summer of 1998. Hubris before the fall!
(Of course there is nothing wrong, and everything right, with a whole bunch of real smart guys carefully poring over kernel code, automated or not, and shaking out as many bugs as possible. Should happen more often.)
Although reliability of missile guidance systems is important, I'd have thought that the military would happily trade a 1% chance of post-launch system failure for things like a bigger payload or a better ability to deal with enemy countermeasures. (And 1% is orders of magnitude worse than today's commercial operating systems would give them).
If this kernel really is a major step in upwards reliabiliy, I would have thought the most likely applications would be civilian. Things like self-driving cars, or civil aviation autopilots and fly-by-wire systems, or automated railway or air-traffic control.
"It's probably a good thing bumblebees put a lot more faith in empirical testing rather than mathematical theorems, and so do I - until it is thoroughly tested in a real environment, nothing is proven."
Nothing is ever proven. Because A has happened n times, you can never be 100% sure that A will happen on the n+1st occurence. You just gain more confidence. Not that I think bumblebees are too worried about their tried and tested technique failing them tomorrow.
Daaaaaiiiiiissssyyyyy daaaaaiiiiisssyyyy, ggiiiiiiveeee meeeee youuurrrrr annsssswwweerrrrr trruuuuuueeeeee. From what I can tell, HAL was never built on the 3 laws of robotics. RoboCop's Prime Directives, maybe. Dick? You're fired!
Ok, stop. There's a truism that applies in situations like this. If I, as a lay-person, can spot a problem with some expert's (or group of expert's) work within 30 seconds of hearing about it, it's fairly likely that they will have thought of it too. This makes nay-saying on that basis pretty pointless. Apart from anything else, it's boring and makes you look like an idiot.
Everyone should really read http://ertos.nicta.com.au/research/l4.verified/proof.pml to see what the researchers are actually claiming, and see if you still think that a kernel which is, for instance, *completely immune* from buffer overflows, pointer errors and memory leaks (given the assumption constraints) is a waste of time.
For my money, *anything* that raises the security bar is a good thing.
You're making the mistake of putting numbers on the wrong side of the equation.
Here:
One beer is 10p (I wish!)
Bulk discount, three beers for 25p.
Three men each put in 9p, thus giving the bartender 27p for three beers - so they get 2p change.
Bartender gets to keep the 2p change (as a tip, presumably). Nothing has gone anywhere.
Don't be confused, vincent is just an idiot that seems to think that a mathematical problem used to trick high school kids is somehow relevant to formal mathematical proofs.
He even suggests C is fundamentally flawed, which is interesting seeing as like 99% of computing systems around today run on it.
C isn't fundamentally flawed, there are just bad programs who can use it incorrectly allowing issues to arise because they simply didn't understand how to program properly.
Can you provide a reference for the aeronautical engineer that proved mathematically that bumble bees cannot fly? No you can't it's an urban myth.
I think the problem is really that mathematical proof is indeed proof ... within certain limits. The proof it the easy bit it's the limits that are the bastard.
The summary on the front page says that this is a Linux kernel; it isn't (there's a clue in it being a microkernel). It can run a para-virtualised version of Linux and - in principle - other operating systems in this way. However, only the functionality provided by this secure kernel is "proven".
We in the chip industry use formal proofs on real projects.
These days we commonly use formal proofs to compare gate level implementations of designs (from automated design tools) with the original design in a high-level language. It offers a much more complete verification than mere simulations. Sounds like this could have been useful on that crappy Viper project (RSRE = loud harmonica).
We also use formal proofs on high-level designs, although these methods have their drawbacks and limitations it has to be said.
Mind you, I would take anything coming from a bunch of Aussie academics with a large pinch of salt. Jeez they can't even spell their own initialisms.
@ vincent himpe
What's your point? The bartender's problem is a matter of "blinding with science". It's works by assuming false premises, and expressing them in such a matter-of-fact way that the listener takes them as given.
In fact, I've been asked variations on the bartender's problem without actually knowing the answer themselves. When I explain how it works, I sometimes find they're so trapped in the illusion that they refuse to accept the answer. (Are you one of these...?)
The thing with computers is that yes, they are reliant on valid input, and false premises programmed in can be a stopping point, but if they have all the appropriate information, their lack of a brain means there's no psychological tricks you can employ to convince them not to explore the full search space.
'When I explain how it works, I sometimes find they're so trapped in the illusion that they refuse to accept the answer.'
I've had the exact same odd experience. Otherwise genuinely intelligent people will say
things like 'this shows that maths is flawed'. I'm sure they're secret celestine prophecy readers, and they are everywhere.
I don't get it. I really don't. A group of people have gone to the trouble of putting together a microkernel that's provably without bugs in the C code, and they're getting slated for it? It's like SpaceX or someone saying "we've invented a rocket that'll get us to Pluto and back in 10 minutes, but we need to fire it up outside the atmosphere", and then everyone taking the piss instead of saying "cool, let's figure out how to get it in the Space Shuttle".
Sure, it requires a known-good C compiler. If you need this for your business, you can work on it. And if you want to move to a new platform, you don't need to develop a whole new microkernel, just a new C compiler. Certainly there are ambiguities in the C language, but they're known and well-documented, which is why coding standards such as MISRA-C exist to guide coders around those ambiguities. (Not heard of MISRA? Then you don't know enough to have an opinion on the subject of safety-critical software.) Actually, optimisation is usually the problem with compilers - provably-correct compilation from a line of C to lines of assembler is fairly straightforward (at least without interrupts getting in the way), but it's slower and less efficient.
@Annihilator: "Nothing is ever proven"? Sorry, but 2+2 still equals 4 and parallel lines don't meet in finite space, regardless of day of the week, phase of the moon, or 50 trillion years in the future. Get a grip.
Hi Hugh - I didn't claim that bumblebees can't fly. I know that it's an urban myth - came from a drunk aeronautical engineer who worked out that a bumblebee can't fly like a conventional fixed wing aircraft. Problem is that they don't try to fly like that - if it stops flapping its wings, it'll fall out the sky - it won't glide.
However, with reverse-pitch semirotar blades they fly just fine.
@Graham Bartlett - 2+2 equals 4 is an extension of the definition/assumption/rule that 1=1 and permutational mathematics. 2+2=4 doesn't "prove" anything. Parallel lines never meeting are again a definition of finite space, and not there to prove anything. Do a maths degree.
Assuming that we can get a fool-proof system, why is the first practical use have to be for a war/military solution?
"The technology is designed for complex embedded systems where reliability is of critical importance, so applications in missiles and other defence-related systems are an obvious application of the software."
How about a system to cure HIV or cancer? How about a way to mass-produce food for drought-ridden countries? Does it have to be for blowing people up?
Grenade icon for the irony.
uhmm.... customers paid 27p, bartender stole 2p - the "oher pence is one of the other 25 the bar is keeping in the til to pay for the drinks.
The incorrect assertion is in the statement where you are taking the total of what the people paid, and adding what the bartender stole - and expecting this for some reason to equal 30.
You also say "they customers paid 27, the bar owner was paid 25 and the bartender stole 2p - that totals up to 54p - where did the extra 24p come from??" If you mis-state the facts and add negatives to positives you can come up with all kinds of numbers.
30p goes in til
5 p comes out
1p goes to each customer (3p)
2p goes in sneaky pete the bartenders pocket
25p left in til,
customers paid 27p
bartender stole 2p
bar get 25 (2 short of what owner wanted)
All this adds up just fine.
Thanks for posting though, I did have to look for a second to find the false statement..... a good mind exercise in being careful what crap you listen too - just look at the US healthscare debate.
Canada's former prime minister Jean Chretien once said,
"No, a proof is a proof. What kind of a proof? It's a proof. A proof is a proof, and when you have a good proof, it's because it's proven."
This has given Canadians much needed hilarity, something sorely missing in our politics and culture.
http://www.canadaka.net/video/293-jean-chretien-a-proof-is-a-proof.html
c is _just_ a language. It allows one to code instructions for a cpu. Get it wrong and it'll hurt you; so will running with scissors. You want I should write a microkernel in vb.NET because it's "manged" and "foolproof" and hides all those scary memory allocations from you ?
meh
(that's not a helicopter, it's a squashed bug)
"A group of people have gone to the trouble of putting together a microkernel that's provably without bugs in the C code, and they're getting slated for it?"
From the Great Book of Lies:
"In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. Functional correctness refers to the input-output behaviour of the algorithm (i.e., for each input it produces the correct output)."
(http://en.wikipedia.org/wiki/Program_specification)
No mention was made in the article that the specification that the code was checked against was similarly proved to be mathematically correct, so really what we've got is a microkernel that's free from coding bugs but not necessarily free from logic-related bugs. Which means you could have a rocket that will always, always, always crash 20m from the launch site even though the customer wanted a long-range ballistic missile.
When the mathematicians can prove the specification is free from fuckwittery and the program is functionally correct that will be a good day. This announcement is merely a guarantee that the build quality is up to the management team's brainstorming sessions.
This post has been deleted by its author
Does the C language have a formally defined specification using mathematical notation?
C has a syntax dependent on context.
Perhaps we should look at our code as a conjecture that requires other people, erm customers, to prove correct or not. But, if there is no spec then the code is not a conjecture but just a programmer's doodling.
Now let's shoot the colonel with void pointers and see what type of wounds we inflict.
C is probably an OK choice. It is a very simple, and therefore verifiable, language.
C++ is way, way, more complex than C. Complexity means failures.
Modula2, erlang and other languages that help detect runtime errors, but that's not really a help: the system still fails. At least when your brakes fail you can die with the knowledge that it was an array bounds exception that killed you.
Others have already corrected you on the bartender problem, so I'll refrain from pointing out that there's no reason why the amount originally paid by the customers minus the change returned to the customers (= price charged for goods plus amount retained by bartender) plus the amount stolen by the bartender (already accounted for) should add up to the amount originally paid by the customers. I should know, I've got an engineering degree (from the days when that entailed more maths than a maths degree) and I've worked in a bar. It's a bit like Abbot and Costello's proof that 13 * 7 = 28.
Your comments on languages also miss the point. How do you know that the compiler for your latest fancy-arsed language is mathematically correct? At least C instructions can be mapped to machine instructions; and the ARM architecture on which they intend to run it is famous for its hardwired instruction set (no microcode). Meaning that there's a mapping from C instructions to logic gates. That's about as verifiable as you can get!