Safety verification for assembly code is attracting more and more attention. On the one hand, high-level programs must be translated before executed on a real machine; compilation or optimization bugs may invalidate the safety guarantee established for the source programs. On the other hand, some applications are distributed (e.g., native code for mobile computation) or even directly written (e.g., core libraries for embedded systems) in assembly code; enforcement at a low-level is a must for them.
I will present a language for certified assembly programming (CAP) as a semi-automatic approach for the static verification of arbitrary safety properties. CAP makes use of a general "type system" that directly supports higher-order logic reasoning. It can be applied to both sequential and concurrent assembly code. The programmer proves the well-formedness of a program with respect to its specification with help of a proof assistant, and the result can be checked mechanically by a proof checker. To demonstrate that proof construction is not unduly difficult, I will explain how we certified a library for dynamic storage allocation. In addition, I will give a brief overview on some latest results and ongoing efforts in the project that help improve the applicability of the approach on a wider scale.
Dr Dachuan's web page is here