BASIL: Boogie Analysis for Secure Information-Flow Logics

Project summary

This project is implementing an information-flow security analysis logic (previously developed by DSTG) on top of the Boogie intermediate language for software verification. This will increase the automation of the approach, and integrate support for the generation of annotations. The analysis technique has been designed by DSTG to provide higher assurance than is available through existing analysis tools. The focus on automation in this project will ensure the tool can be incorporated into current software development processes with minimal cost and effort.

Partner organization(s)