[OLPC Security] bitfrost - formal analysis & implementation

[Frank Ch. Eigler]

Hi -

A brief scan of the newly released bitfrost specification shows a lot
of effort has gone into this fairly complex system.  This and the BIOS
upgrade procedures outlined separately appear to strike a plausible
balance between the "no lock-down" slogan and the practical needs of
theft deterrence, user registration, secure software updating.

Has any thought been given to possibly probing this design for subtle
security problems using a formal modeling system such as CycSecure
or PVS or similar projects?

Another question.  I may have just missed this in the specs, but how
many implementation aspects have been nailed down?  What mixture of
enforcement layers are envioned (selinux, discretionary user-space
libraries, server processes)?  Have interactions with custom-installed
"non-participating" software such as ordinary linux command-line
binaries / compilers been analyzed?

- FChE