Complete and Efficient Checks for Branching-Time Abstractions

Lead Research Organisation: Imperial College London
Department Name: Dept of Computing

Abstract

Computer programs, electronic control units in cars, model-driven development in software engineering, and non-linear feedback systems within biological cells are all examples of dynamical systems or processes that benefit greatly from their capture in formal models and subsequent analysis of such models. Model creation aids documentation, system comprehension and can facilitate change management. Model checking, an analysis of a model with respect to a fixed property, can gain important insights into subtleties of the dynamical systems these models represent, enabling system validation with predictive power.Automated or semi-automated model generation and analysis are necessary for any realistic technology transfer of model checking into industrial use contexts. Barriers to such technology transfer are foremost due to the lack of scalability (model checks are either undecidable or take too must time and space) and to the lack of full automation of existing model-checking methodology. Another barrier is that existing approaches cannot deal with more complex properties that mix path quantifiers but are needed in modern application contexts, e.g. A system can always reach a state from which a certain cyclic reaction is possible.'' This research creates a model-checking framework that addresses these barriers directly for this full range of complex properties: scalability through the ability to reduce all model checks to those with finite-state and small models; and automation through an extension of existing predicate-abstractiontechniques, notably the counter-example-guided abstraction refinement (CEGAR), to this setting of more complex properties.This research programme will also be carried out for quantitive systems in which the dynamics of a system is governed by probability distributions.To summarize, the main aim of this proposal is to develop a framework for efficient modelling, checking, and refining of abstractions that are complete (i.e. one can always discover compliance or non-compliance of a system with any property through some finite-state abstraction) and precise (i.e. the abstract model enjoys a maximum number of properties that are true in the system it abstracts) for properties that appeal to branching time and probabilities.

Publications

10 25 50
 
Description We found a robust and intuitive way of combining security policies, for example those from different organizations, so that we can automatically detect and conflicts or inconsistencies in these policies, check whether some policies refine others, and detect where policies may need to be repairs to address issues stemming from such compositions. This is vital for understanding how federations of businesses can have a consistent security posture.

We also developed novel abstraction techniques for the automatic verification of systems, both qualitative and probabilistic ones, where successful proof of a property as well as successful refutation of a property shown on an abstraction of a system transfer to the system itself. In particular, this discovered that popular property patterns allow for precise and efficient verification of abstractions by simple rephrasing of properties so as to eliminate the imprecision resulting from reasoning over abstractions.

The findings about are especially valuable and deep when considering probabilistic systems, and they may have provided a new perspective on an open problem, the satisfiability of a popular and important probabilistic temporal property language.

We also developed a novel way of specifying and enforcing access control based on relationships (as opposed to attributes that individuals possess), by showing how modal logic and its model checking problem naturally supports this.
Exploitation Route Please see our descriptions of further impact, both academic and non-academic, in other parts of this report.
Sectors Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Security and Diplomacy

 
Description The work on 3-valued policy composition influenced thinking about quantitative policies and their composition in the assessment of security and trust in systems and processes. This had impact with Intel in that they funded a project to explore this aspect further, and it had impact with AWE, who become interested in these methods in the context of arms control verification. This also led to funding we now have with AWE, and the work done on that PhD project will be reported at SET for BRITAIN 2016 -- with an accompanying AWE press release.
First Year Of Impact 2012
Sector Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Financial Services, and Management Consultancy,Security and Diplomacy
Impact Types Societal,Economic,Policy & public services

 
Description Debating Tools for Social Networks: Future Intelligent Recommender Systems
Amount £26,094 (GBP)
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 07/2012 
End 12/2012
 
Description Integrating Security Protocol Analyzers into Undergraduate Curricula
Amount $49,039 (USD)
Organisation Intel Corporation 
Sector Private
Country United States
Start 10/2012 
End 09/2013
 
Description Trust Evidence
Amount $165,644 (USD)
Organisation Intel Corporation 
Sector Private
Country United States
Start 10/2012 
End 09/2014
 
Description Bell Labs 
Organisation Alcatel-Lucent
Country France 
Sector Private 
PI Contribution We provided expertise in 3-valued model checking and formal reasoning, when studying the problem of designing intuitive yet formally executable and analysable languages for composing access control policies.
Collaborator Contribution Dr Bruns and his team at Bell Labs provided expertise in Computational Logic, and in logic-based approaches to access control (where Dr Bruns was coPI on a related grant from the US National Science Foundation).
Impact We published in top international conference (IEEE CSF) and journals (ACM TISSEC) the findings of our research. This collaboration was also instrumental for transferring research insights from the grant EP/E028985/1 from settings that were more concerned with software verification to applications that were more concerned with security policies, their specification, analysis and enforcement. The collaboration also helps the PI Huth to gain international recognition as a researcher in computer security, and it thus laid the foundation for future funding in that area.
Start Year 2006
 
Description Kim Larsen 
Organisation Aalborg University
Country Denmark 
Sector Academic/University 
PI Contribution We provided the initial research questions and reported key results informally at TACAS 2007, which the PI Huth co-chaired. Kim Larsen and his team attended the conference and we discovered common interests and complementary expertise. Our contribution was in the formulating the strategy of this research activity, and in proving some of the hard results.
Collaborator Contribution Larsen's team managed to add more results to this research programme, and they also provided the connection to the EATCS and its Bulletin, which led to an invited column there, reporting on our joint findings.
Impact We managed to publish in leading international conference (e.g. FOSSACS) and journals (e.g. EATCS Bulletin and CUP Mathematical Structures in Computer Science. The collaboration also helped with the visibility of the research carried out under these EPSRC grants, as Kim Larsen is arguably the best known computer scientist in Denmark with global visibility.
Start Year 2007
 
Description Royal Holloway 
Organisation Royal Holloway, University of London
Country United Kingdom 
Sector Academic/University 
PI Contribution We made contact with Prof Jason Crampton at a Workshop in Denmark where the PI Huth gave a keynote based on research from the Grant EP/E028985/1. This first meeting resulted in collaborations in which we brought in expertise from Formal Methods, Model Checking, and 3-valued approaches to said areas.
Collaborator Contribution Prof Jason provided expertise in access control architectures, languages, and in particular for the industry standard XACML.
Impact We published several research papers in top conferences (e.g. ESORICS 2010) and leading international journals (e.g. Springer's Software Tools for Technology Transfer). This collaboration also was chiefly responsible for conceiving the Dagstuhl Seminar "Verifiably Secure Process-Aware Information Systems", please see http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=13341 for which we are in the process of editing a book to be published in Springer.
Start Year 2008
 
Title PCTL and games 
Description We developed new techniques for reasoning for verifying probabilistic systems using model checking. The novelty is in capturing the truth semantics which forms the specification of model checking semantics in terms of two-person games. This lead to the conception of a new form of automaton, which accepts an entire Markov chain. 
Type Of Technology New/Improved Technique/Technology 
Year Produced 2010 
Impact These insights led to better abstraction techniques in model checking for a probabilistic temporal logics (PCTL) and opened up a new line of attack on the open problem of whether satisfiability of that logic PCTL is decidable. 
 
Title Semantic minimization 
Description 3-valued model checking allows for sound refutation and verification of properties based on abstraction. But its compositional algorithm may return "don't know", trading off precision of analysis with complexity of analysis. We discovered that most practically relevant properties are such that the generally less precise compositional algorithm is probably precise for such properties -- this securing the best of both possible worlds (efficient *and* precise analysis). 
Type Of Technology New/Improved Technique/Technology 
Impact This led to a collaboration with Patrice Godefroid, where we extended this study to the modal mu-calculus and published the findings in the top logic conference IEEE LICS 2005.