Camp 2011 - Version 1.4

Chaos Communication Camp 2011
Project Flow Control

Andreas Bogk
Day Day 3 - 2011-08-12
Room Baikonur
Start time 22:30
Duration 01:00
ID 4426
Event type Lecture
Track Science
Language used for presentation English

Certified programming with dependent types

Because the future of defense is liberal application of math

Dependent types expand the concept of types in programming languages by arbitrary predicates depending on the value of the type. This lecture will introduce the concept and show how it can be used to develop formally verified code.

As part of this lecture, a PDF parser written using the described methods will be released. Initial tests show that produces excellent results in distinguishing between legitimate PDFs and those with malicious payloads, with a rejection rate for malicious PDFs exceeding 95%.