Oct 252017
 

I’m at ISSRE 2017 in Toulouse, France, for the presentation of our paper on Interactive Runtime Verification and attending the talks of the day.

Our paper on Interactive Runtime Verification (i-RV) can be downloaded here.

Verde, our open-source tool for i-RV, can be retrieved and experimented with our interactive tutorial by following this link. Our interactive tutorial illustrates how i-RV can be used to more effectively debug C programs leveraging runtime verification.

Aug 102017
 

Our journal paper entitled Decentralized Enforcement of Document Lifecycle Constraints has been accepted for publication in Information Systems, an Elsevier journal.

Below is an abstract of the paper:

Artifact-centric workflows describe possible executions of a business process through constraints expressed from the point of view of the documents exchanged between principals. A sequence of manipulations is deemed valid as long as every document in the workflow follows its prescribed lifecycle at all steps of the process. So far, establishing that a given workflow complies with artifact lifecycles has mostly been done through static verification, or by assuming a centralized access to all artifacts where these constraints can be monitored and enforced. We present in this paper an alternate method of enforcing document lifecycles that requires neither static verification nor single-point access. Rather, the document itself is designed to carry fragments of its history, protected from tampering using hashing and public-key encryption. Any principal involved in the process can verify at any time that the history of a document complies with a given lifecycle. Moreover, the proposed system also enforces access permissions: not all actions are visible to all principals, and one can only modify and verify what one is allowed to observe. These concepts have been implemented in a software library called Artichoke, and empirically tested for performance and scalability.

This is joint work with Sylvain Hallé, Raphaël Khoury, Quentin Betty from Université du Quebec at Chicoutimi, and Antoine El-Hokayem from Univ. Grenoble Alpes.

Jul 172017
 

The paper entitled GREP: Games for the Runtime Enforcement of Properties has been accepted for publication in the proceedings of ICTSS 2017, the 29th IFIP International Conference on Testing Software and Systems.

Below is an abstract of the paper:

We present GREP, a tool for the runtime enforcement of (timed) properties. GREP takes an execution sequence as input (stdin), and modifies it (stdout) as necessary to enforce the desired property, when possible. GREP can enforce any regular timed property described by a deterministic and complete Timed Automaton. The main novelties of GREP are twofold: it uses game theory to improve the synthesis of enforcement mechanisms, and it accounts for uncontrollable events, i.e. events that cannot be controlled by the enforcement mechanisms and thus have to be released immediately. We present an overview of GREP and validate its usability with a performance evaluation.

This is joint work with Matthieu Renard and Antoine Rollet from University of Bordeaux.

The pre-print of the paper can be downloaded here.

Jul 152017
 

The paper entitled Interactive Runtime Verification has been accepted for publication in the proceedings of ISSRE 2017, the 28th International Symposium on Software Reliability Engineering (ISSRE) – IEEE. ISSRE will be held in Toulouse (France), October  23-26, 2017.

Below is an abstract of the paper:

Runtime Verification consists in studying a system at runtime, looking for input and output events to discover, check or enforce behavioral properties. Interactive debugging consists in studying a system at runtime in order to discover and understand its bugs and fix them, inspecting interactively its internal state.

Interactive Runtime Verification (i-RV) combines runtime verification and interactive debugging. We define an efficient and convenient way to check behavioral properties automatically on a program using a debugger. We aim at helping bug discovery and understanding by guiding classical interactive debugging techniques using runtime verification.

This is joint work with Raphaël Jakse, Jean-François Méhaut, and Kevin Pouget from Univ. Grenoble Alpes.

The preprint of the paper can be downloaded here.

Jul 012017
 

Our paper entitled Verifying Policy Enforcers has been accepted for publication in RV 2017, the 17th international conference on Runtime Verification.

Below is the abstract of the paper:

Policy enforcers are sophisticated runtime components that can prevent failures by enforcing the correct behavior of the software. While a single enforcer can be easily designed focusing only on the be- havior of the application that must be monitored, the effect of multiple enforcers that enforce different policies might be hard to predict. So far, mechanisms to resolve interferences between enforcers have been based on priority mechanisms and heuristics. Although these methods provide a mechanism to take decisions when multiple enforcers try to affect the execution at a same time, they do not guarantee the lack of interference on the global behavior of the system.
In this paper we present a verification strategy that can be exploited to discover interferences between sets of enforcers and thus safely identify a-priori the enforcers that can co-exist at run-time. In our evaluation, we experimented our verification method with several policy enforcers for Android and discovered some incompatibilities.

This is joint work with Oliviero Riganelli, Daniela Micucci, Leonardo Mariani from University of Milano Bicocca.

Jun 252017
 

The paper entitled “From high-level modeling toward efficient and trustworthy circuits” has been accepted for publication in Software Tools for Technology Transfer, a Springer journal.

Below is an abstract of the paper:

Behavior–interaction–priority (BIP) is a layered embedded system design and verification framework that provides separation of functionality, synchronization, and priority concerns to simplify system design and to establish correctness by construction. BIP framework comes with a runtime engine and a suite of verification tools that use D-Finder and NuSMV as model-checkers. In this paper, we provide a method and a supporting tool that take a BIP system and a set of invariants and compute a reduced sequential circuit with a system-specific scheduler and a designated output that is true when the invariants hold. Our method uses ABC, a sequential circuit synthesis and verification framework, to (1) generate an efficient circuit implementation of the system that can be readily translated into FPGA or ASIC implementations and to (2) verify the system and debug it in case a counterexample is found. Moreover, we generate a concurrent C implementation of the circuit that can be directly used for runtime verification. We evaluated our method with two benchmark systems, and our results show that, compared to existing techniques, our method is faster and scales to larger sizes.

The paper is now online on Springer Website.

One can also download the pre-print of the paper.

This is joint work with Fadi A. Zaraket, and Mohamad Jaber from American University of Beirut and Mohamad Noureddine from University of Illinois at Urbana Champaign.

 

May 302017
 

The paper entitled THEMIS: A Tool for Decentralized Monitoring Algorithms has been accepted as a tool-demonstration paper to ISSTA 2017, the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ISSTA 2017 will be held in Santa Barbara, California, USA, on July 10–14, 2017.

Below is an abstract of the paper:

THEMIS is a tool to facilitate the design, development, and analysis of decentralized monitoring algorithms; developed using Java and AspectJ. It consists of a library and command-line tools. THEMIS provides an API, data structures and measures for decentralized monitoring. These building blocks can be reused or extended to modify existing algorithms, design new more intricate algorithms, and elaborate new approaches to assess existing algorithms. We illustrate the usage of THEMIS by comparing two variants of a monitoring algorithm.

The pre-print of the paper can be downloaded on my publications Webpage.

THEMIS is open-source and available for download at https://gitlab.inria.fr/monitoring/themis.

This is joint work with A. El-Hokayem, Univ. Grenoble Alpes, Inria.

Apr 292017
 

The paper entitled Monitoring Decentralized Specifications has been accepted for publication in the proceedings of ISSTA 2017, the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, which will be held in Santa Barbara, California, USA, on July 10–14, 2017.

The abstract of the paper is below:

We define two complementary approaches to monitor decentralized systems. The first relies on those with a centralized specification, i.e, when the specification is written for the behavior of the entire system. To do so, our approach introduces a data-structure that i) keeps track of the execution of an automaton, ii) has predictable parameters and size, and iii) guarantees strong eventual consistency. The second approach defines decentralized specifications wherein multiple specifications are provided for separate parts of the system. We study decentralized monitorability, and present a general algorithm for monitoring decentralized specifications. We map three existing algorithms to our approaches and provide a framework for analyzing their behavior. Lastly, we introduce our tool, which is a framework for designing such decentralized algorithms, and simulating their behavior.

The pre-print of the paper can be downloaded on my publications Webpage.

This is joint work with Antoine El-Hokayem (Univ. Grenoble Alpes, Inria, Laboratoire d’Informatique de Grenoble).

Apr 172017
 

The paper entitled Formal analysis and offline monitoring of electronic exams has been accepted for publication in Formal Methods in System Design, a Springer journal.

The abstract of the paper is below:

More and more universities are moving toward electronic exams (in short e-exams). This migration exposes exams to additional threats, which may come from the use of the information and communication technology. In this paper, we identify and define several security properties for e-exam systems. Then, we show how to use these properties in two complementary approaches: model-checking and monitoring. We illustrate the validity of our definitions by analyzing a real e-exam used at the pharmacy faculty of University Grenoble Alpes (UGA ) to assess students. On the one hand, we instantiate our properties as queries for ProVerif, an automatic verifier of cryptographic protocols, and we use it to check our modeling of UGA exam specifications. ProVerif found some attacks. On the other hand, we express our properties as Quantified Event Automata (QEAs), and we synthesize them into monitors using MarQ, a Java tool designed to implement QEAs. Then, we use these monitors to verify real exam executions conducted by UGA. Our monitors found fraudulent students and discrepancies between the specifications of UGA exam and its implementation.

The preprint of the paper can be downloaded here.

This is joint work with Ali Kassem (Inria Grenoble) and Pascal Lafourcade (University of Clermont).

Apr 162017
 

The paper entitled Runtime Enforcement Using Büchi Games has been accepted for publication in SPIN 2017, the 24th International SPIN Symposium on Model Checking of Software.

Below is an abstract of the paper.

We leverage Büchi games for the runtime enforcement of regular properties with uncontrollable events. Runtime enforcement consists in modifying the execution of a running system to have it satisfy a given regular property, modelled by an automaton. We revisit runtime enforcement with uncontrollable events and propose a framework where we model the runtime enforcement problem as a Büchi game and synthesise sound, compliant, and optimal enforcement mechanisms as strategies. We present algorithms and a tool implementing enforcement mechanisms. We reduce the complexity of the computations performed by enforcement mechanisms at runtime by pre-computing decisions of enforcement mechanisms ahead of time.

The preprint of the paper can be downloaded here.

This is joint work with Matthieu Renard and Antoine Rollet from University of Bordeaux (France).