Authors: Pavel Avgustinov, Kevin Backhouse and Man Yue Mo
Paper Information
Title: | Variant analysis with QL |
Authors: | Pavel Avgustinov, Kevin Backhouse and Man Yue Mo |
Proceedings: | FM FMComplete |
Editors: | Jan Peleska, Klaus Havelund and Bill Roscoe |
Keywords: | program analysis, variant analysis, declarative programming, logic programming, security |
Abstract: | ABSTRACT. As new security problems and innovative attacks continue to be discovered, program analysis remains a burgeoning area of research. However, writing new analyses has remained a specialist task, and although declarative and logic programming has been observed to be an excellent fit for phrasing complex analysis, the goal of democratising the creation of new checks has remained elusive. QL builds on previous work to use Datalog for this purpose, but solves some of the traditional challenges: Its object-oriented nature enables the creation of extensive libraries, and the query optimiser minimises the performance cost of the abstraction layers introduced in this way. QL enables agile security analysis, allowing security response teams to find all variants of a newly discovered vulnerability. Their work can then be leveraged to provide automated on-going checking, thus ensuring that the same mistake never makes it into the code base again. We will introduce the principles behind QL, and show how we can perform declarative variant analysis on high-profile open-source code bases. |
Pages: | 5 |
Talk: | Jul 17 14:30 (Session 121C: FM I-Day) |
Paper: |