Verification of Concurrent and Higher-Order Recursive Programs

Lead Research Organisation: Royal Holloway, University of London
Department Name: Computer Science

Abstract

Global society increasingly relies on devices controlled by software, from TV
sets to vehicle braking systems. It is considered a "fact-of-life" that
software contains errors, which can come at great cost, such as the Mars Polar
Lander crash or the 1992 failure of the London Ambulance Dispatch Service. In a
2008 study, the US NIST agency estimates faulty software costs the US economy
$59.5bn annually.

Classically software is tested by running it under as many difficult situations
as possible. However, it is not feasible to run a program under all
environments. Hence, testing relies on the perspicacity of the testing engineer
who must carefully choose environments that may expose flaws.

Modern computers increase performance by allowing many computer programs to run
concurrently. Anticipating the interactions of even as a little as two programs
is an extremely difficult task, and errors are often difficult to replicate and
diagnose. Furthermore, the efficiency of hardware is often increased by
permitting behaviours a software developer would not expect.

An alternative approach to ensuring correctness is model-checking.
Model-checking attempts to use fully automatic techniques to prove that a
program behaves as expected under all conditions. This area has flourished
recently, including a 2007 Turing Award for Clarke, Emerson and Sifakis, who
transformed the technique from a theoretical pursuit into an industrially
applicable product. Model-checking is embraced by companies like Microsoft (to
improve its Windows OS) and Altran-Praxis (for safety-critical software).

However, model-checkers must rely on simplified models of computer programs to
guarantee results, leading to many correct programs being labelled erroneous.
This is a design choice, following the argument that it it better to raise a
false alarm, than let an error pass by.

However, a large number of false alarms damage reliability and usability --- a
software developer will not study reported errors carefully if the majority are,
in fact, not errors at all. This is a real problem in the large scale
deployment of such tools. The goal of this fellowship is to increase the
precision of verification tools --- reducing the number of false alarms ---
while retaining the efficiency of current techniques, resulting in
model-checking tools that are more reliable and usable.

During this fellowship, we will construct a state-of-the-art verification
framework, unifying several prototypical tools and requiring novel
model-checking techniques, and permitting new ideas to be experimented with
quickly. The framework will be tested on real-world software to ensure its
usability and reliability. It will accurately model difficult programming
paradigms, such as modern concurrent behaviours and "higher-order" constructs
(increasingly embraced by state-of-the-art programming languages).

The research will be carried out at Imperial College London, and will bring
together researchers at Oxford University, Universite Paris-Est, and Universite
Paris-Diderot as well as the CARP project, based across several universities and
companies world-wide, and researchers at Microsoft Research, Cambridge.

Planned Impact

It is well known that the majority of the software development effort goes on
maintenance and bug repair. The use of verification techniques during
development reduces the prevalence of errors, and thus, reduces development
time. In addition to the speed of delivery, the use of verification techniques
allows companies to provide improved support and maintenance packages.

UK companies will benefit from the results of this fellowship in two ways.
First, since the framework is developed in the UK, they will have easy
face-to-face access to the development team. Secondly, by educating UK students
about the tools, UK companies will benefit from improved programming practices
in the graduates they employ. Especially as concurrent programming becomes more
important, having techniques to quickly identify concurrency bugs (which are
difficult to find and reproduce, yet simple to make) will be an enormous
advantage.

Furthermore, software is ubiquitous in modern society. Thus, the erroneous
nature of programming projects affects everyone in many ways, ranging from minor
annoyances when a laptop has to be rebooted, to weaknesses exploitable by
writers of malevolent software, business critical software such as web-services,
and more potentially more serious situations with safety critical software, such
as car braking systems. An improved quality of software will have a wide
benefit.

The impact of the fellowship will be ensured through a number of means.

First, in addition to enabling cutting-edge research, the construction of a
model-checking framework will unify many related research activities under a
single name. This will promote recognition and awareness of the framework by
stakeholders, facilitating communication outside of academia.

The framework itself will take as input programs written in suitable languages,
such as Java and C++, and produce useful output, rather than the ``expert-only''
output produced by prototypical tools. This is a facility demanded by potential
industrial partners who will not tolerate a ``by-hand'' modelling process. By
providing these features, the ease-of-use of verification tools will be assured,
allowing new ideas to be tried by non-expert users in both the industrial and
open-source communities.

To ensure the distribution of the framework, and its real-world applicability,
we will first ensure that a web-site is set up. This site will provide the
downloads of the framework, instructions for users, and bug-reporting/feature
request facilities. Then, we will experiment with the framework on open-source
software, such as Linux. The results of these experiments can then be
communicated to the software developers --- for example, through bug reports, if
bugs are found. This communication will raise awareness of our tools and we
will encourage software developers to try the tools themselves, providing
valuable feedback for further improvements. In addition, we may analyse
open-source code produced by companies as a pathway into industry.

Experiments with open-source software will demonstrate the effectiveness of the
framework. These results will be used when contacting software companies who
will be interested in using our tools. Initially this may include firms such as
Microsoft who are already involved in developing verification tools of their
own. Further companies may be approached during, for example, industry liaison
events held at Imperial, or directly.

Finally, as a keen teacher, on completion of the fellowship, I will seek to
present lecture courses on verification. By exposing students to model-checking
techniques and tools, the next generation of programmers will be equipped to
transport these techniques to their future work environment. This take-up, I
believe, will increase as tools become more accurate and scalable, and as the
difficulties in concurrent programming become a daily issue for developers.

Publications

10 25 50
publication icon
A. Carayol And M. Hague (2014) Saturation algorithms for model-checking pushdown systems in International Conference on Automata and Formal Languages (AFL)

publication icon
A. Carayol And M. Hague (2014) Regular Strategies in Pushdown Reachability Games in Reachability Problems (RP)

publication icon
Broadbent C (2013) C-SHORe

publication icon
C. Broadbent, A. Carayol, M. Hague And O. Serre (2013) C-SHORe: A Collapsible Approach to Higher-Order Verification in International Conference on Functional Programming (ICFP)

publication icon
Carayol A (2014) Saturation algorithms for model-checking pushdown systems in Electronic Proceedings in Theoretical Computer Science

publication icon
Chen T (2018) What is decidable about string constraints with the ReplaceAll function in Proceedings of the ACM on Programming Languages

publication icon
Chen T (2019) Decision procedures for path feasibility of string-manipulating programs with complex operations in Proceedings of the ACM on Programming Languages

publication icon
Hague M (2017) Collapsible Pushdown Automata and Recursion Schemes in ACM Transactions on Computational Logic

publication icon
Hague M (2019) CSS Minification via Constraint Solving in ACM Transactions on Programming Languages and Systems

publication icon
Hague M (2016) Reachability Problems

 
Description We have developed the automata-based approach to the verification of higher-order recursive programs, including implemented verification software, and techniques and theoretical verification results for concurrent higher-order recursive programs, showing many cases of decidable properties for differing models of concurrency.

We have also showed that the automata-based approach to pushdown systems (first-order programs) can be used to optimise web pages, including an implemented tool. This work was further pursed to introduce a new minimisation technique for web style sheets, also including an implemented minimisation tool.

Finally, in the latter stages of the project, the focus shifted to solving, via automata, string constraints, which is a key bottleneck in the analysis of modern languages, such as JavaScript, which are both higher-order and make frequent use of strings.
Exploitation Route Our findings have already been taken forward by a group in Japan who have developed the most efficient higher-order program analysis tool (currently), HorSat.

Our theoretical results may be built on to improve the state-of-the-art in verifying concurrency properties of higher-order programs.

Our web-optimisation work provides a framework and semantics under which greater minimisation may be obtained that the simple syntactic rewritings currently used as standard.

Finally, our string analysis work provides techniques and a constraint solver which may be used by any verification tool wishing to handle strings (such tools frequently make use of constraint solvers that can handle the data their programs use).
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software)

URL https://pure.royalholloway.ac.uk/portal/en/persons/matthew-hague%28c4baa4a0-192e-49c8-a699-feda6a04a583%29.html
 
Description The findings have been published in the world-leading conferences Principles of Programming Languages 2016, Object Oriented Programming, Systems Languages and Applications 2015, Computer Science Logic / Logic in Computer Science (CSL-LICS) 2014, The International Conference on Functional Programming (ICFP 2013), Foundations of Software Technology and Theoretical Computer Science (FSTTCS) 2013, Reachability Problems (RP) 2014 and Automata and Formal Languages AFL, 2014. Techniques we have introduced have also been taken up by Naoki Kobayashi's group in Tokyo and published in the renowned conference on Concurrency (CONCUR) 2013. We have also produced a tool (C-SHORe) for reachability checking of sequential higher-order recursion schemes (models of higher-order programs) implementing our research which is available from http://cshore.cs.rhul.ac.uk. We have also developed a tool for the analysis of JQuery programs, as well as a tool for the minimisation of Cascading Style Sheets, for web-programming. Collaborative research related to the project has also informed the development of the new TLS protocol, which was verified as part of work supervised during this project.
First Year Of Impact 2013
Sector Digital/Communication/Information Technologies (including Software),Education
Impact Types Cultural,Societal

 
Description Google Faculty Research Award
Amount $54,302 (USD)
Organisation Google 
Department Research at Google
Sector Private
Country United States
Start  
 
Description Symbolic Analysis of Higher-Order Programs 
Organisation École Normale Supérieure de Cachan
Country France 
Sector Academic/University 
PI Contribution Supervision of a research student summer project verifying Haskell programs by using symbolic execution on the result of compiling the code.
Collaborator Contribution Mario Alvarez Picallo visited as a research student for a summer project experimenting with symbolic execution engines on the compiled code from Haskell programs.
Impact A proof-of-concept tool was produced that showed some success in analysing higher-order programs.
Start Year 2015
 
Description Verification of Concurrent Haskell 
Organisation Royal Holloway, University of London
Country United Kingdom 
Sector Academic/University 
PI Contribution I will be supervising a PhD. student from the Information Security Group's Centre for Doctoral Training for the duration of his studies.
Collaborator Contribution A PhD. student.
Impact Initial work on formal verification of higher-order programs led to a workshop publication in FTfjP at ECOOP 2016. The research then led on to work formalising and verifying the new version of the TLS security protocol. This work led to publications in the top-ranked CCS (2017) conference.
Start Year 2014
 
Description Verification of Concurrent Higher-Order Programs 
Organisation Royal Holloway, University of London
Country United Kingdom 
Sector Academic/University 
PI Contribution Use of visit funding for Fu Song (who could not come) to fund a visit by Vincent Penelle. We worked together on furthering the verification aims of the project.
Collaborator Contribution Work on and publication of a paper in Reachability Problems 2018.
Impact Publication in RP 2018 on Constrained Dynamic Tree Networks.
Start Year 2016
 
Title C-SHORe 
Description The tool performs reachability analysis of higher-order recursion schemes and collapsible pushdown systems, which are a model of higher-order programs. 
Type Of Technology Software 
Year Produced 2013 
Open Source License? Yes  
Impact The tool was the first to implement an automata based approach to the verification of higher-order recursion schemes. It also was the first to use a "saturation" method. The tool showed that this approach is competitive with existing approaches and inspired a further tool (HORSAT) to be produced by Naoki Kobayashi's group in Tokyo, using similar techniques. 
URL http://cshore.cs.rhul.ac.uk
 
Title OSTRICH 
Description An expressive constraint solver for string constraints using replaceAll, transducers, &c. 
Type Of Technology Software 
Year Produced 2018 
Open Source License? Yes  
Impact None. 
URL https://github.com/pruemmer/ostrich
 
Title SatCSS 
Description Tool for minimisation of Cascading Style Sheets for web-site optimisation. 
Type Of Technology Software 
Year Produced 2018 
Impact None. 
URL https://github.com/matthewhague/sat-css-tool
 
Title TreePed 
Description A tool implenting an algorithm for identifying redundant CSS rules in HTML5 applications. Provides a complete interface for the underlying program model, but only a rudimentary translation from jQuery programs. 
Type Of Technology Software 
Year Produced 2015 
Impact Research tool. 
URL https://bitbucket.org/TreePed/treeped