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.
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.
Organisations
Publications
| Description | So far, the work funded through this award has produced two new methods for the evaluation of machine learning systems. In particular, these methods evaluate whether a machine learning system is robust, in the sense that it can still give the correct output even if changes are made to its input. The methods developed focus on evaluating robustness to meaningful changes to the inputs, rather than the somewhat artificial changes considered by much of the existing literature. As well as these two methods, there has also been a significant empirical finding: machine learning systems that are specifically trained to be more robust to the artificial input tweaks usually considered are in fact much less robust to the more meaningful changes to the input. This emphasises the importance of considering exactly what robustness properties we require of our machine learning systems before we can confidently deploy them. |
| Exploitation Route | Further research is likely to build upon the outcomes of this funding. Further ahead, tools for the evaluation of machine learning systems that draw on this research may be built. |
| Sectors | Digital/Communication/Information Technologies (including Software) |