| Ken, a good example. For those of you who want to reach much further
| back, Paul Karger told me of a similar problem in the compiler (I don't
| remember the language) used for compiling the A1 VAX VMM kernel, that
| optimized out a check in the Mandatory Access Control enforcement, which
| separates information of different classifications (*). [For those not
| familiar with it, this was a provably secure kernel on which you could
| host multiple untrusted operating systems. Despite what some young-uns
| seem to think, VMs are not a new concept - they go back at least three
| decades that I know of, and possibly longer. The A1 VAX effort ended
| roughly 20-25 years ago, to give a timeframe for this particular
| compiler issue.]
The VAX VMM effort died with the announcement of the Alpha, in late 1992
- though obviously the death was decided internally once the move to
Alpha was decided, which would have been somewhat earlier. The origins
of the VAX VMM effort date back to the early 80's.
As best I can recall, the VAX VMM kernel was written almost entirely in
PL/I. (Why? Because the main alternatives available at the time were
assembler and C - way too open-ended for you to be able to make useful
correctness assertions - and Pascal, which even in VMS's much extended
version was too inflexible. There were almost certainly a few small
assembler helper programs. Before you defend C, keep in mind that this
is well pre-Standard, when the semantics was more or less defined by "do
what pcc does" and type punning and various such tricks were accepted
practice.)
I know from other discussions with Paul that it was understood in the
high assurance community at the time that, no matter what you knew about
the compiler and no matter what proofs you had about the source code,
you still needed to manually check the generated machine code.
Expensive, but there was no safe alternative. So any such optimizations
would have been caught.
-- Jerry
| --Jeremy
|
| (*) At least that's what my memory tells me - if Paul is on this list,
| perhaps he can verify or correct.
_______________________________________________
Secure Coding mailing list (SC-L) SC-L@securecoding.org
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php
SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com)
as a free, non-commercial service to the software security community.
_______________________________________________
