Modular Verification of Control-Flow Properties of Program with Procedures(MCVPP)

Introduction

MCVPP is a sub-proejct of the CVPP project. In the CVPP project we aim to develop an algorithmic approach for verification of open systems . An open systems is a system which some components are available with their implementations while other components are available by their specification . Specification of a component contains a formal description of its essential properties. Open systems are important in case of modular design where specification of components in used for verification since the implementation might be changed in the future, and/or for mobile code where the implementation of some components is not available at the time of verification.

For more information about the CVPP project please read Dilian Gurov's page about CVPP.

Participants

• Dilian Gurov, KTH
• Siavash Soleimanifard, KTH
• Marieke Huisman, University of Twente
• Afshin Amighi, University of Twente

Tasks

• A. Case srtudy on modular verification with CVPP
• Find a Java program with interesting global behavioral safty property
Possible case studies
• Door access control system, a system containing two interfaces for method calls. The internaces are "Locked" and "Unlocked". The internded global security property to be checked is that internal method invocations(e.g., change password) cannot be done via "Locked" interface.
• Java servlet controller
• Java API protocol, i.e., security of Java program by sequence of API calls
• Dvice driver
• Java enterprise model, e.g., JavaBeaans
• AccountAccessor application of the java smart card samples
• An interesting global property of AccountAccessor is: "after calling beginTransaction arrayCopyNonAtomic cannot be called until commitTransaction or abortTransaction is called"
• Flow graph model of the application is generated
• The structural method specification of each method is extracted in the format of CCS
• CCS specifications translated to simulation logic
• Maximal models generated by two methods
• Generating maximal model from simulation logic structural formula by maximal model generator tool of CVPP tool-set
• Generating maximal model by automata product of CCS and maximal model of the method interface
• Compose maximal models
• Generate PDS model of composed maximal models and model check against global behavioral propery
• JavaPurse application of the java smart card samples
• Specify behavioral specification of each method
• Reduce the behavioral specification to structural specification and construct maximal flow-graph for each method
• Automate the reduction process
• Compose all combinations of the constructed maximal flow-graphs and the extracted flow-graph of the program and model check the resulting model against global specification
• Chek if the methods specifications are met by global specification
For behavioral specification
• Specify the Java program as PDS
• Generate flow-graph of the program
• Convert the flow-graph to a pushdown system model
• Automate the conversion
• Model check PDS against global specification
• B. Use Boolean programs as component model
• Extract Boolean program of a componenet
• Model check the Boolean program against global specification