C-rusted: A Formally Verifiable Flavor of C for the Development of Safe and Secure Systems

C-rusted is an innovative technology whereby C programs can be (partially) annotated so as to express: ownership, exclusivity and shareability of language, system and user-defined resources; properties of objects and the way they evolve during program execution; optional types, nominal types and subtypes compatible with any C data type. The annotated C programs, being fully compatible with all versions of ISO~C, can be translated with unmodified versions of any C compiler. The crucial point is that such annotations express program properties that can be formally verified through static analysis: if the static analyzer flags no error, then the annotations are provably coherent among themselves and with the annotated C code, in which case the analyzed program portions are provably exempt from a large class of logic, security, and run-time errors. The annotation system has been designed not to be intrusive: in most of the situations, also the lack of annotations has a precise meaning that is used by the static analyzer to formally verify program properties. C-rusted is a pragmatic and cost-effective solution to up the game of C programming to unprecedented integrity guarantees without giving up anything that the C ecosystem offers today. That is, keep using C, exactly as before, using the same compilers and the same tools, the same personnel\dots but incrementally adding to the program the information required to formally verify correctness, using a system of annotations that is not based on complex formalisms (such as mathematical logic) and can be taught to programmers in a week.