Machine Learning for Verification.

Lead Research Organisation: University of Oxford
Department Name: Computer Science

Abstract

A growing challenge for today's semiconductor industry is the efficient and correct co-design of hardware alongside low-level software, especially in system-on-chip design. To meet today's productivity objectives, formal HW/SW co-verication needs to scale to pre-silicon exploration of system-wide scenarios. This project's success would facilitate such scaling, allowing semiconductor manufacturers to have greater confidence in their systems' correctness at a lower cost.

Aims and objectives
In previous work at Oxford, this problem was attacked by creating whole-system models (including both hardware and software) as groups of `lightweight software threads', which could then be analysed working together as a single concurrent program. In the next phase of work, we will investigate the use of modern machine-learning techniques to mine higher-level `scenario models' from execution traces of a virtual platform model of the system, running a real application load. This will aim to be largely automatic and to create generalised models that cover a significant group of system behaviours, rather than simply the state interactions of a particular hardware device execution. Most important, the abstraction will be directly driven by a real application load, exercising 'use cases' of interest. Currently, we are conducting a pilot study based around ARM's trusted firmware for the A-class processors. We have developed trace-generating instrumentation for this platform. In the next phase of work, we will survey the applicable machine-learning techniques and select the most promising candidates for experimentation. We will survey the available industrially-developed structures for high-level modelling, and design a suitable representation that gets to the essence of the required semantics and is simple and general. We will leverage Oxford's strengths in language design and formal semantics to create a modelling framework that is as practical and semantically clean as possible. Finally, we will conduct experiments to validate this approach, preparing publications on the results.

Novelty of the research methodology
As of yet, there has been little application of machine learning approaches to improve the efficiency and efficacy of verification. In particular, we are not aware of any work attempting to use machine learning to mine virtual platform execution traces for the creation of system models where the abstraction is maximally relevant to intended use cases, as described above.

Alignment to EPSRC's strategies and research areas
The project directly relates to the Verication and Correctness research area. Furthermore, it aligns well with the council's three current strategic goals within the area. First, the project forges links with the research area of Articial Intelligence Technologies (another of Oxford's strengths) in order to scale verication up to more complex, larger-scale systems. Second, in accordance with Strachey's philosophy, the project aims to address real-world challenges faced by industry through complementary work on theoretical insights and practical tools and experiments. Third, the project contributes to the reduction of security risks by increasing the confidence that there are no exploitable bugs in the systems in question.

Isaac Dunn, Natasha Jeppu, Tom Melham and Daniel Kroening will collaborate on the project at Oxford. ARM and Intel will also be involved in the project: their system designs will be used, they will provide valuable input on the problems currently faced in industry, and they will be kept up to date with the progress of the project.

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/R513295/1 01/10/2018 30/09/2023
2052803 Studentship EP/R513295/1 01/10/2018 30/09/2022 Isaac Dunn