Proof-Carrying Code (Seminar)

Organizer:

Prof. Dr. Heiko Mantel

Registration:

in the MAIS secretary (S2|02, E318)

Preparation Meeting:

Wednesday, 13.04.2011, 16:30 in S2|02, A213

Schedule:

Friday, 27.05.2011, 9:00-11:15 in S2|02, A313

Topic

A user downloaded a software from the Internet, in general, cannot easily check whether the software meets the properties that the manufacturer promises. Many of these properties could be mathematically specified, and it could be formally proven that the software fulfills them. Such a proof, however, is a tedious work and requires human and computational resources.

The idea of the Proof-Carrying Code (PCC) is to accompany the software with a proof certificate, using which the claimed properties of the software could be verified. Although, issuing such a certificate appears to be a complex task, checking of the proof stored in the certificate is much easier and could be done automatically.

In the seminar we will consider articles contributing to the techniques and applications of the PCC principle, e.g., checking the security of Java bytecode by means of security type systems.

The participants of the seminar could use an opportunity to apply the studied PCC techniques in the Lab course "Proof-Carrying Code on Mobile Devices" which will take place in the same semester.

Learning Material

Please visit the internal page.

Last modified on 22 October 2012.