An Abstract Semantics Tool for Secure Information Flow of Stack-based Assembly Programs

We present a tool supporting the verification of programs written in stack-based assembly language against the secure information flow property. First, the tool builds the transition system, which corresponds to an abstract execution of the program, embodying security information and abstracting from the actual values. Then the states of the abstract transition system are checked to detect the satisfaction of the secure information flow property. The tool offers a windows user interface, through which the user can control the verification process, and observe the intermediate and final results.