Program Analysis Cell

Project summary

The DSTG Program Analysis Cell investigates the use of formal methods and program analysis for detecting software security vulnerabilities. The aim is to develop advanced tools and techniques for the simultaneous development of cyber-secure systems and the associated assurance evidence necessary to prove the systems’ lack of vulnerabilities and flaws, and resistance to attacks. The emphasis of the research is on general techniques, rather than specific solutions, allowing for a diversity of solutions and innovation to be supported. This will lead to cybersecurity principles that will endure as systems and attacks evolve into the future.

Areas of research include:

Formal security foundations - developing a formal understanding of the effects of multicore hardware, operating systems, and compilation processes on information security.

Advanced program analysis - developing automated techniques for finding security vulnerabilities during software development and evolution.

Secure software development - establishing a tool/language ecosystem supporting vulnerability analysis of software at the source code, binary and intermediate levels.

Partner organization(s)