Constructing Trusted Code Base
These days
it is possible to run a
C compiler or
an operating system that
are designed and implemented so that they work correctly for sure.
You can learn how to use techniques that led to these
achievements
in this course.
The page of the course in USOSweb
is here
(in Polish)
or here (in English).
Grading
Joint grade that takes into account software project and exam in proportion 45% and 55% respectively.
Lectures
- Introduction: risk analysis, applications, existing verified software
lecture 1, lecture 2,
lecture 12, lecture 13
- Programs extracted from proofs - logical basis
lecture 3 and Coq sources,
lecture 4 and more Coq sources
- Formalization of a procedure to be extracted (Coq)
lecture 5 and more Coq sources
- Verification of specification-annotated programs - logical basis
Why3 sources for lecture 6;
lecture 7 and its examples and additional materials and yet more additional materials;
lecture 8
- Program verification - an example (Why3)
a bigger example for the lecture 9,
lecture 10 (on TFTP)
- Certification and other tools
lecture 14
Assignemts
- Work on removing complaints by splint in the
TFTP implementation.
- The assignment to prove in Coq is here.
- Environment to start work with Frama-C/Why3 is here.
Final exam
There will be some at some point.
This course receives financial
support from the Intel Corporation
via the Intel Labs Security
Curriculum Initiative.