30 Aug
2014
30 Aug
'14
9:26 a.m.
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
31 Aug
31 Aug
12:26 a.m.
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(a)luv.asn.au
http://lists.luv.asn.au/listinfo/luv-talk
1:17 a.m.
Memories!
The Real-Time Operating System of MARS
http://home.iitj.ac.in/~saurabh.heda/Papers/Research%20Papers/1988/RTOS%20o…
"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(a)luv.asn.au
http://lists.luv.asn.au/listinfo/luv-talk
_______________________________________________
luv-talk mailing list
luv-talk(a)luv.asn.au
http://lists.luv.asn.au/listinfo/luv-talk
1:54 a.m.
--------------------------------------------
On Sun, 31/8/14, Douglas Ray <dougray(a)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.)
3134
days inactive
3135
days old
3 comments
3 participants
participants (3)
-
David E Payne -
Douglas Ray -
Rohan McLeod