Secure and Bug Free ?
Assembled Cognoscenti; I thought the following tale in which Linux turned out to be the insecure element; might be of amusement. In a conversation with a gentleman at the Nicta "TechShowCsae2014" yesterday; http://www.eventbrite.com.au/e/nicta-tech-showcase-2014-tickets-12119157727?... he was explaining his group's interest in secure and bug-free software; in the context of 'mission-critical' applications; particularly OS's. I thought 'mission-critical' had something to do with the military and large corporation's; but it turned out they are primarily looking at the OS's in vehicles and air-craft. Apparently there have been recent cases of the "OS's' of cars being cracked remotely; via the wireless immobilizing system and the brakes etc. being operated remotely ! Regardless; the story seemed to be that as aircraft move from mechanical to electrical control and from there to fly-by-wire and then fly-by-fiber networks; (removing hundreds of kilo-meters of fire prone complex, heavy wiring in the process); a huge requirement for secure and bug-free OS's arose. Since sequential bug removal is not a practical option :-) What he seemed to be claiming was his group had written a RT OS in C; and then compiled it for ARM processors. Where things seemed to become interesting was 1/ the C code was apparently subject to some kind of mathematical analysis which 'somehow' checked the code's logical integrity against the specification ? (Is this possible ?) 2/ the machine code from the compiler was then checked against the specification ? - I have no idea what this means !; anyway the assumption is that the compiler may introduce bugs, security holes. Apparently the resulting RT OS has very little functionality, which is remedied by supplying that functionality via Linux VM's Anyway to get to the end of the tale; where Linux turned out to be the insecure element !; they are employing 'Red-Teams' (Tiger-teams ?) of hackers to 'crack' the Linux VM's. This is not just pie-in-the sky stuff either; they had a quad-copter with such an add-on OS; as proof of concept. Apparently the OS is available as open-source and binary for ARM and x86 CPU's, but not in the above secure form at: http://sel4.systems regards Rohan McLeod
On 30/08/14 9:26 AM, Rohan McLeod wrote:
Assembled Cognoscenti; I thought the following tale in which Linux turned out to be the insecure element; might be of amusement. In a conversation with a gentleman at the Nicta "TechShowCsae2014" yesterday;
http://www.eventbrite.com.au/e/nicta-tech-showcase-2014-tickets-12119157727?...
he was explaining his group's interest in secure and bug-free software; in the context of 'mission-critical' applications; particularly OS's. I thought 'mission-critical' had something to do with the military and large corporation's;
but it turned out they are primarily looking at the OS's in vehicles and air-craft.
Apparently there have been recent cases of the "OS's' of cars being cracked remotely; via the wireless immobilizing system and the brakes etc. being operated remotely ! Regardless; the story seemed to be that as aircraft move from mechanical to electrical control and from there to fly-by-wire and then fly-by-fiber networks; (removing hundreds of kilo-meters of fire prone complex, heavy wiring in the process); a huge requirement for secure and bug-free OS's arose. Since sequential bug removal is not a practical option :-)
What he seemed to be claiming was his group had written a RT OS in C; and then compiled it for ARM processors. Where things seemed to become interesting was 1/ the C code was apparently subject to some kind of mathematical analysis which 'somehow' checked the code's logical integrity against the specification ? (Is this possible ?)
I don't know when the "real time" paradigm changed, but I remember in the 80s real-time OS research focused on verifiable time constraints rather than "do everything as fast as possible". To specify, analyse and verify a RT OS requires a model and then implementing the test points and synchronisation mechanisms. Establishing models and test methodologies was where RT research was at that time. I came across something called "MARS" in from Technische Uni, Vienna - one of their postgrads gave a talk at my uni, '88 or '89. The incongruity is that a verifiably RT OS is necessarily slower than an unverifiable "as fast as possible, please" coding strategy. You can ensure deadlocks do not happen, and that time-critical events are guaranteed. But if you need peak performance - what used to be called RT - you do not want a verifiably RT OS.
2/ the machine code from the compiler was then checked against the specification ? - I have no idea what this means !;
Wikipedia: "Formal Verification"
anyway the assumption is that the compiler may introduce bugs, security holes. Apparently the resulting RT OS has very little functionality, which is remedied by supplying that functionality via Linux VM's Anyway to get to the end of the tale; where Linux turned out to be the insecure element !; they are employing 'Red-Teams' (Tiger-teams ?) of hackers to 'crack' the Linux VM's. This is not just pie-in-the sky stuff either; they had a quad-copter with such an add-on OS; as proof of concept. Apparently the OS is available as open-source and binary for ARM and x86 CPU's, but not in the above secure form at: http://sel4.systems
regards Rohan McLeod
_______________________________________________ luv-talk mailing list luv-talk@luv.asn.au http://lists.luv.asn.au/listinfo/luv-talk
Memories! The Real-Time Operating System of MARS http://home.iitj.ac.in/~saurabh.heda/Papers/Research%20Papers/1988/RTOS%20of... "This paper gives a short overview of the architecture of the distributed real-time system MARS (MAintainable Real-Time System) and describes the design and implementation of its operating system. The main purpose of the MARS kernel is to achieve a timely execution of hard real-time tasks and to provide an efficient communication mechanism suitable for distributed real-time systems." Their current work is at ti.tuwien.ac.at On 31/08/14 12:26 AM, Douglas Ray wrote:
On 30/08/14 9:26 AM, Rohan McLeod wrote:
Assembled Cognoscenti; I thought the following tale in which Linux turned out to be the insecure element; might be of amusement. In a conversation with a gentleman at the Nicta "TechShowCsae2014" yesterday;
http://www.eventbrite.com.au/e/nicta-tech-showcase-2014-tickets-12119157727?...
he was explaining his group's interest in secure and bug-free software; in the context of 'mission-critical' applications; particularly OS's. I thought 'mission-critical' had something to do with the military and large corporation's;
but it turned out they are primarily looking at the OS's in vehicles and air-craft.
Apparently there have been recent cases of the "OS's' of cars being cracked remotely; via the wireless immobilizing system and the brakes etc. being operated remotely ! Regardless; the story seemed to be that as aircraft move from mechanical to electrical control and from there to fly-by-wire and then fly-by-fiber networks; (removing hundreds of kilo-meters of fire prone complex, heavy wiring in the process); a huge requirement for secure and bug-free OS's arose. Since sequential bug removal is not a practical option :-)
What he seemed to be claiming was his group had written a RT OS in C; and then compiled it for ARM processors. Where things seemed to become interesting was 1/ the C code was apparently subject to some kind of mathematical analysis which 'somehow' checked the code's logical integrity against the specification ? (Is this possible ?)
I don't know when the "real time" paradigm changed, but I remember in the 80s real-time OS research focused on verifiable time constraints rather than "do everything as fast as possible".
To specify, analyse and verify a RT OS requires a model and then implementing the test points and synchronisation mechanisms.
Establishing models and test methodologies was where RT research was at that time. I came across something called "MARS" in from Technische Uni, Vienna - one of their postgrads gave a talk at my uni, '88 or '89.
The incongruity is that a verifiably RT OS is necessarily slower than an unverifiable "as fast as possible, please" coding strategy. You can ensure deadlocks do not happen, and that time-critical events are guaranteed.
But if you need peak performance - what used to be called RT - you do not want a verifiably RT OS.
2/ the machine code from the compiler was then checked against the specification ? - I have no idea what this means !;
Wikipedia: "Formal Verification"
anyway the assumption is that the compiler may introduce bugs, security holes. Apparently the resulting RT OS has very little functionality, which is remedied by supplying that functionality via Linux VM's Anyway to get to the end of the tale; where Linux turned out to be the insecure element !; they are employing 'Red-Teams' (Tiger-teams ?) of hackers to 'crack' the Linux VM's. This is not just pie-in-the sky stuff either; they had a quad-copter with such an add-on OS; as proof of concept. Apparently the OS is available as open-source and binary for ARM and x86 CPU's, but not in the above secure form at: http://sel4.systems
regards Rohan McLeod
_______________________________________________ luv-talk mailing list luv-talk@luv.asn.au http://lists.luv.asn.au/listinfo/luv-talk
_______________________________________________ luv-talk mailing list luv-talk@luv.asn.au http://lists.luv.asn.au/listinfo/luv-talk
-------------------------------------------- On Sun, 31/8/14, Douglas Ray <dougray@cpan.org> wrote: Doug, if you're the muso bloke I used to see at FIG etc. long ago, hello! ' I don't know when the "real time" paradigm changed, but I remember in the 80s real-time OS research focused on verifiable time constraints rather than "do everything as fast as possible".' SNIP DP: I think like many other terms eg. "hacker", it means different to different people and the ones who know the least about the subject are also likely to not know that. (Like "bit" used to be abbreviated to "B" & "byte" to "b"; now it's usually the other way round but you have to know that you'll have to guess or work out which, or you may misunderstand someone else & never realise you did.)
participants (3)
-
David E Payne -
Douglas Ray -
Rohan McLeod