back to article Secure microkernel that uses maths to be 'bug free' goes open source

A nippy microkernel mathematically proven to be bug free*, and used to protect drones from hacking, will be released as open source tomorrow. The formal-methods-based secure embedded L4 (seL4) microkernel was developed by boffins backed by National ICT Australia (NICTA). In 2012, the software was enlisted to help stop hackers …

Silver badge

18+ hoursTo Go

I'm glad someone is doing this work. It'll be interesting to see the reqs given I have this as the minimum here. [Except mine is ground ased as my flying leaves a LOT to be desired.]

3
1
Silver badge

Re: 18+ hoursTo Go

"A microkernel differs from monolithic kernels – such as the Linux and Windows kernels"

The Windows kernel isn't monolithic. It's a hybrid microkernel.

0
0
Anonymous Coward

Compiler and runtime(s) also guaranteed defect free?

Or does it just need a senior "engineering" manager to declare them trustworthy, or else?

Viper. gcc code-generation buglist. To name but two.

Still, it may well be a step in the right direction.

9
0
Silver badge
Facepalm

Re: Compiler and runtime(s) also guaranteed defect free?

> gcc

> formally verified

TFW. Choose one.

1
0
Silver badge
Thumb Up

Re: Compiler and runtime(s) also guaranteed defect free?

Linus has just sent off another expletive-laden missive because gcc 4.9.0 does silly things when compiling the Linux kernel. Then later on it was found that the bug goes all the way back to 4.5.0 but something else was changed in 4.9.0 so the bug happens more often.

8
0
Anonymous Coward

Re: Compiler and runtime(s) also guaranteed defect free?

"TFW. Choose one."

Point taken, but WTF is TFW?

0
0

This post has been deleted by its author

This post has been deleted by its author

Silver badge

Re: Compiler and runtime(s) also guaranteed defect free?

They could use Greenhill's compiler, that's very good and is formally developed. It's the foundation of their INTEGRITY operating system (see this Wikipedia entry, which as a customer I think is also very good. Not cheap, but is value for money, if you see what I mean.

I suppose this new microkernel is a direct competitor to the kernel inside INTEGRITY, though of course there's more to a complete and usable OS than just the kernel.

0
0

Re: Compiler and runtime(s) also guaranteed defect free?

Time for Wine

0
0
Terminator

Ignores hacking attempts and keeps going...

How long till it ignores control attempts from fleshies altogether and does the Logical Thing by itself?

10
0
Anonymous Coward

Re: Ignores hacking attempts and keeps going...

Too long. But we live in hope.

1
0
Boffin

Technically speaking...

Windows uses a microkernel architecture as well. It's just hard to tell under all the layers of proprietary.

3
2
Anonymous Coward

Re: Technically speaking...

Yes, if by "use" you mean "originally show some influence of but since then more or less disregard". Think display driver in kernel.

18
1
Silver badge

Re: Technically speaking...

That's due to one of the trade-offs of microkernels: performance.

1
0
Silver badge

Re: Technically speaking...

Was it really necessary for MS to change the architecture of the NT kernel just so a server OS could have all-singing all-dancing display drivers?

9
1
Silver badge

Re: Was it really necessary for MS to change

For marketing yes, and that ultimately won along with a lot of legacy-supporting crud and mind-numbing stupidity like making IE deeply embedded.

If they had stuck to the original microkernel approach as planned by Dave Cutler and just accepted the performance penalty then it would have been one of the most secure OS around.

9
1
Anonymous Coward

Re: Technically speaking...

benchmark performance may benefit from Gates' diktat re graphics.

Realworld productivity? Robustness is often more important. Gates loses.

1
1
Silver badge

Re: Was it really necessary for MS to change

No, it still wouldn't be very secure. The Windows kernel might have been more secure, but only a fraction of Windows security issues have had to do with the Windows kernel anyway.

3
1

Re: Technically speaking...

Think display driver in kernel.

BTW, this is no longer the case as of Windows Vista (IIRC; might be Win7).

I can personally verify this as I've had my video driver crash hard under Windows 7 a number of times (faulty card.) The screens go all blank then come back up and Windows displays a little pop-up telling you that the video driver crashed but was reloaded.

2
0
Roo
Devil

Re: Technically speaking...

"Was it really necessary for MS to change the architecture of the NT kernel just so a server OS could have all-singing all-dancing display drivers?"

Yes it was, because they couldn't bring themselves to copy the UNIX way of achieving the same end efficiently and (more) securely. ;)

3
3
Anonymous Coward

Re: Technically speaking...

"this is no longer the case as of Windows Vista (IIRC; might be Win7)."

I think it's Vista too. It had to be done so that Windows could offer a Trusted Computing Platform. Not one that could be trusted by end users and IT departments, but one that could be trusted by the "content industry" to provide an end to end tamper-proof copy-protected platform for the delivery of "high value rich media content".

2
1

Is there a Microsoft parallel to Godwin's Law?

No matter what the subject, the thread turns into a MS bash-fest within a few posts...

Not that I don't think MS should be protected from a kicking.... and I am partial to putting in a boot myself.

5
0
Coffee/keyboard

Re: Is there a Microsoft parallel to Godwin's Law?

That's gotta be the post of the day.

0
0
Go

Re: Is there a Microsoft parallel to Godwin's Law?

No matter what the subject, the thread turns into a MS bash-fest within a few posts...

Proof that if Eadon didn't exist, commentardery would create one

1
0
Anonymous Coward

Re: Technically speaking...

It also had to do with driver robustness. Vista introduced a new driver model with some additional safeguards included. That's why video driver updates don't always have to force a restart (because now the video driver is less-attached to the kernel itself, allowing it to be stopped and restarted). It's still kernel-space stuff for performance reasons, but IIRC it's more compartmentalized.

1
0
Silver badge

Re: Is there a Microsoft parallel to Godwin's Law?

Pehaps that's what we should call it from now on:

Eadon's Law: As an online discussion grows longer, the probability of a comparison involving Microsoft or its executives approaches 1.

0
0
Silver badge

Re: Technically speaking...

"Think display driver in kernel."

Most of it runs in User mode in Windows: https://docs.microsoft.com/en-us/windows-hardware/drivers/display/windows-vista-and-later-display-driver-model-architecture

0
0
Silver badge

Re: Technically speaking...

"Was it really necessary for MS to change the architecture of the NT kernel just so a server OS could have all-singing all-dancing display drivers?"

They didn't change the kernel at all. They changed the display driver architecture. The micro kernel was not changed by that.

0
0
Bronze badge

To quote….

seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees.

Sorry……..

Just don't see it…., even clock/edge jitter is enough to make the above statement complete nonsense.

It might be totally 'provable' when it's all neatly packaged up in its mathematical simulator but then go completely tits up in the real world due to boundary conditions in hardware clocking.

2
11
Silver badge

Ever thought they took that into consideration?

4
1
Silver badge

"has provable upper bounds on interrupt latencies"

Er, those upper bounds would include hardware jitter as that is a known value and generally much much smaller than the software steps in ISR task-swapping.

3
0
Anonymous Coward

Please go do some homework….

http://www.researchgate.net/publication/258998077_An_Experimental_Study_on_Execution_Time_Variation_in_Computer_Experiments

0
0
Silver badge

CPU

If they have a proven secure Microkernel, I assume they've proved that their hardware (including CPU) are all secure too.

1
0
Silver badge

Re: CPU

You have to consider each aspect separately. All they have proven is the implemented logic of the microkernel meets the specifications.

You can have bugs and flaws in:

- Specifications

- Sub-systems called by the microkernel

- Compiler

- Standard Libraries

- CPU/FPU hardware

But compared the today's huge kernels in Linux/UNIX/Windows/etc which have the last three as well as a box-of-frogs evolved design, that provability is a big start to something reliable for critical jobs.

4
0
Silver badge

Re: CPU

Why assume anything? If they had proved all their hardware was secure, would you have lead with "I assume they've proved their kernel is secure too"?

Even if they haven't, it is one tick box off on the way to proving every component is secure, which is note- and praiseworthy surely?

2
0
Anonymous Coward

Re: CPU

"Even if they haven't, it is one tick box off on the way to proving every component is secure, which is note- and praiseworthy surely?"

Well, it may indeed prove to be one tick box off on the way to a secure system, but in some ways it's the smallest (and therefore easiest) part to do.

Writing a compiler, run time library (nb the kernel may very well not use any library code) and designing the hardware are arguably much larger and more expensive jobs. Particularly the hardware; formally designing a fast-ish CPU is going to be $Billions.

The micro kernel is going to be only a few thousand lines of code (pure guess, but it is micro). Compilers and runtime libraries have many more lines of code than that, and they too need to be correct.

It will be interesting to see it though.

0
0
Silver badge

Still vulnerable to hacking

But only via the high speed lead projectile vector.

2
0

Re: Still vulnerable to hacking

The preferred method at the moment is via the GPS system whether by directly hacking in or by spoofing it with a local mobile GPS station. Do not forget that the Iranians were the first to 'Hijack' a RQ-170 drone, it is alleged that the Yugoslavians and others were good at 'downing' some of the earleir beasts.

Now a secure kernel is fine, but what about the myriad of software and hardware connected to it?

2
1
Holmes

Re: Still vulnerable to hacking

>But only via the high speed lead projectile vector.

And don't forget the "failure to change the default admin password" vector.

4
0
Silver badge

Re: Still vulnerable to hacking

We don't know for certain they hacked it. Besides, the drone was military tech, so you'd think they'd be using the encrypted military GPS. Cracking military security tech would be a first-order coup and something MANY antagonistic countries would be itching to get, bit Iran's keeping mum, which tells me their method was likely much more prosaic and specific.

0
0

GPS hacking: I call bollocks

It is easy to go to the supermarket, buy a role of tinfoil and hit the forums claiming that GPS is just a bunch of radio waves and can thus be hacked.

I worked for a about 12 years devloping GPS systems, including some time deep in the analysis and design of the actual GPS tracking algorithms.

Sparing you all the maths and theory, there's so much stuff you'd have to fiddle with and get amazingly precisely right that it makes spoofing GPS almost immpossible outside well controlled lab conditions.

In theory it is possible, in practice rather more likely not!

1
0
Anonymous Coward

"what about the myriad of software and hardware connected to it?"

Wrt the GPS example: if the beancounters permitted it, an inertial guidance system retained alongside the GPS would have stood a good chance (albeit not 100%) of bypassing or at least detecting GPS-fiddling.

Or maybe a dual-GPS setup using two of: US GPS, European GPS (Galileo), Russian GPS (Glonass).

Engineers know how to fix things. What do beancounters know?

2
0
Anonymous Coward

Engineers know how to fix things. What do beancounters know?

I recall hearing this story, but I've not been able to find any evidence to back this up:

Some management consultants were working at Amstrad. Alan Sugar walked past a room where a management consultant was talking to an engineer about a product he was working on. The consultant was drilling the engineer over his choice of a particular component due to it's high cost compared to all the other components in the product. The engineer kept on telling the consultant that the component was the only one that would do the job, and the consultant was adamant that their must be a cheaper component he could us instead. Later that day, the management consultants were told to leave and not come back.

0
0

"Later that day, the management consultants were told to leave and not come back."

My experience of Amstrad products would suggest that they fired the engineers.

7
0
Silver badge

I recall hearing this story, but I've not been able to find any evidence to back this up:

...this wouldn't happen to be some sort of perverted form of the 3Com LAN card anecdote, would it?

0
0

The Iranian GPS drone hack is mostly considered an urban legend these days, I believe. Iran loves to make things up, this for example:

http://en.wikipedia.org/wiki/Qaher-313

1
0
JLV
Silver badge
Boffin

>Engineers know how to fix things. What do beancounters know?

Since we are talking about military drones and military procurement in this instance, when have beancounters ever had much to say about military hardware?

$500 Multidirectional Kinetic Injectors (hammers)?

$150M and up "budget affordable due to procurement scale" (the original intent) F-35 fighters?

how many $B to refit Her Majesty's new carriers with supposedly contractually possible catapult extensions?

I don't mind the beancounter bashing vs engineers, usually.

With military procurement however, I think a lot more beancounting sanity checks should be happening. Keeping the same defense budgets, that should result in much better gear for the boys n girls in the frontlines and less gouging by the military contractors.

If it makes engineering sense (and I doubt your Glonass idea makes any sense on NATO gear), then inertial sensors will be fitted in. Whether that is at reasonable cost is quite another question.

1
0
Silver badge

Re: >Engineers know how to fix things. What do beancounters know?

That's also an urban myth. Army quartermasters themselves have revealed these to just be accounting generalities meant to get paperwork through. Sure, people complain about the $500 hammer, but then there's the $600 jet engine...

0
0

Will it run Crisis?

2
0

Page:

POST COMMENT House rules

Not a member of The Register? Create a new account here.

  • Enter your comment

  • Add an icon

Anonymous cowards cannot choose their icon

Biting the hand that feeds IT © 1998–2018