Topic 1
You do not have the permission to view discussions in this forum
Section outline
-
Contents
- Computer Programs/Systems as Subjects of Formal Reasoning
- Introduction (4 on 1)
- Fehler im System: der Traum von Software ohne Bugs (restricted)
- The Language of Logic (4 on 1)
- Specifying and Verifying Sequential Programs
- Hoare Calculus and Predicate Transformers (4 on 1)
- An Axiomatic Basis for Computer Programming (restricted)
- Specifying and Verifying Java Programs
- The Java Modeling Language: Part 1 (4 on 1)
- The Java Modeling Language: Part 2 (4 on 1)
- Proof of Correctness of Data Representations (restricted)
- Extended Static Checking with ESC/Java2 (4 on 1)
- Verifying Java Programs with KeY (4 on 1)
- Specifying and Verifying Concurrent Systems
- Modeling Concurrent Systems (4 on 1)
- Specifiying Properties of Concurrent Systems (4 on 1)
- Verifying Concurrent Systems (4 on 1)
- clientServer.txt, clientServer-mutex.ltl, clientServer-progress.ltl
- roads.txt, roads.ltl
- protocol.pn, clientServer.pn
- Abstrakte Kunst: Fehler finden durch Model Checker (restricted)
- Proof-Carrying Code (PCC)
A class given by Hans-Wolfgang Loidl (LMU Munich), member of the EmBounded project and of the former Mobile Resource Guarantees project.
Proof-carrying-code (PCC) is a software mechanism that allows a host system to determine with certainty that it is safe to execute a program supplied by an untrusted source. This is achieved by attaching a condensed version of a formal proof to the program. In this part of the course we will examine the principles of PCC, explore different variants in the design of a PCC infrastructure, and take a closer look at some selected PCC infrastructures.
The structure of this part of the course is as follows:- Motivation
- Basic Concepts
- An Example: CCured
- Components of the PCC Architecture
- Main challenges
- PCC for Resources
- Certificate Generation
- Summary
The password to this area is handed out in class