FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Variant analysis with QL

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: