[eros-arch] Proof Carrying Code

[Norman Hardy]

Princeton's PCC project: 
<http://www.cs.princeton.edu/sip/projects/pcc/> addresses the 
question of when machine code confines itself to capability 
discipline by its nature, rather than having the discipline 
dynamically imposed. PCC (Proof Carrying Code) is the rubric.
It is much like my largely undocumented tuncol but they have carried 
it much further.
It is a direct offshoot of Necula's PCC.
Much of their work presumes a Java foundation and thus suffers as does E.
They don't use "capability" but the ideas seem to come from lambda calculus
and amount to the same thing.

It would seem to complement both E and EROS (type safe drivers in the kernel).
They seem unaware of the contribution of capabilities to security but 
instead seem to follow Java's mechanisms.

There is much jargon in some of their papers, but perhaps less than 
some older contributions.

-- 
Norman Hardy  <http://cap-lore.com/>