CS252 and CS263 Fall 2000 Project

Verification architecture for proof carrying code

Jaein Jeong ( jaein@cs.berkeley.edu )
Johnathon Jamison ( jjamison@cs.berkeley.edu )

 

We proposed "Verification architecture for proof carrying code" by the suggestion of Prof. John Kubiatowicz. Generally, one would expect to have a processor always give a correct result. Now, a given processor may not be guaranteed to operate correctly due to transient faults. Therefore, the computations made by the processor must be checked. We will take proof carrying code, and have a second processor verify the primary processor's result by comparing it with the proof. Further, this additional processor could monitor many primary processors. Hopefully, the performance cost of having the secondary processor will be offset by other factors.
 
 

Report:

Final report (HTML, PDF)

Progress:

Week Title
1st (30 Oct ~ 5 Nov) Scope of the project (PPT, PDF)
2nd (6 Nov ~ 12 Nov) Base model, Measure of Comparison (PPT, PDF)
3rd (13 Nov ~ 19 Nov) Installation of SimpleScalar (PDF)
4th (20 Nov ~ 26 Nov)  
5th (27 Nov ~ 3 Dec)  
6th (4 Dec ~ End) Presentation (PPT)

 

Links:

SimpleScalar: Simulation Tools for Microprocessor and System Evaluation (Framed Version)

SimpleScalar: Simulation Tools for Microprocessor and System Evaluation (Non-framed Version)

Proof-Carrying Code (Prof. George Necula)

An annotated bibliography on Proof-Carrying Code
 
 

References:

 [1] "Safe Kernel Extensions Without Run-Time Checking". George C. Necula, Peter Lee. Presented at OSDI'96,October 1996.
[2] Steven K. Reinhardt and Schubhndu S. Mukherjee, "Transient Fault Detection via Simultaneous Multithreading"
[3] Todd M. Austin, "DIVA: A Reliable Substrate for Deep Submicron Microarchitecture Design"
[4] "Research on Proof-Carrying Code for Untrusted-Code Security".
George C. Necula and Peter Lee. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, Oakland, 1997.
[5] "Proof-Carrying Code ". George C. Necula. Presented at POPL97, January 1997.
[6] Todd Austin and Doug Burger, "SimpleScalar Tutorial".