[OLPC Security] bitfrost - formal analysis & implementation

[Ivan Krstić]

Hi Frank,

Frank Ch. Eigler wrote:
> 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?

not yet. Perhaps somewhat later.

> I may have just missed this in the specs, but how
> many implementation aspects have been nailed down?  

Every item that made it into the Bitfrost spec did so only after I knew
(in pretty substantial detail) how we're going to be implementing it,
but there are rounds of internal review and test implementations that I
want to complete before I publicly discuss the implementation in detail.
The current schedule is for there to be another open spec in late March
that fully explains the implementation aspects.

Cheers,

-- 
Ivan Krstić <krstic at solarsail.hcs.harvard.edu> | GPG: 0x147C722D