Thomas Sewell1
1Chalmers University, sewell@chalmers.se
Computer software is usually written in one language (the source language) and translated from there into the native binary language of the machine which will execute it. Most operating systems, for instance, are written in C and translated by a C compiler. If the correctness of the computer program is important, we must also consider the correctness of the translation from source to binary.
In the first part of this talk, I will introduce the SydTV tool which validates the translation of low-level software from C to binary. In the specific case of the seL4 verified OS software, this validation combines with the existing verification to produce a trusted binary.
The time taken to execute a program is normally considered to be a property of the final binary rather than the source code. Some programs have essential timing constraints, which ought to be checked by some kind of analysis. In the second part of this talk, I will show how the SydTV translation analysis can be reused to support a timing analysis on the seL4 binary. This design permits the timing analysis to make use of type information from the source language, as well as specific guidance provided at the source level by the kernel developers.