The C standard formalized in Coq - Robbert Jan Krebbers [ING]

The C standard formalized in Coq

You are not allowed to view links. Register or Login

The C programming language was created by Thompson and Ritchie around 1970 as the implementation language of the Unix operating system. The development of Unix demonstrated the efficiency and portability of C, and following that success, C quickly became a dominant general purpose programming language. More than 40 years after its introduction, C remains among the most widely used programming languages in the world. However, despite its continuing wide use, C is also among the most bugprone programming languages in the world. As a result of weak static typing and the absence of run-time checks, it is very easy for C programs to have bugs that make the program crash or behave badly in other ways. Dangling pointers and NULL pointers can be dereferenced, arrays can be accessed outside their bounds, etc.

A recent example is the Heartbleed bug in the widely used OpenSSL cryptography library where a buffer overflow allowed access to arbitrary data, which may contain passwords. Heartbleed is not an incidental case where the unsafety of C has disastrous consequences. Wang et al. have shown that the unsafety of C is a serious problem. In safer programming languages than C, bugs like these are less likely to occur, but due to the performance, control and portability benefits of C, the use of C and C derivatives like C++ remains widespread.

Formal verification is a promising approach to retain the performance, control and portability benefits of C but without the dangers of its unsafety. In formal verification one uses mathematical methods to obtain the highest level of assurance of a program’s safety, or even of its entire functional correctness.

Formato: PDF
Idioma: Ingles

You are not allowed to view links. Register or Login