arXiv subjects

César Sánchez

Publications and source records attributed to César Sánchez.

28 records · Page 2Linked to original sources

arXiv2020

Verifying Hyperliveness

HyperLTL is an extension of linear-time temporal logic for the specification of hyperproperties, i.e., temporal properties that relate multiple computation traces. HyperLTL can express information flow policies as well as properties like symmetry in mutual exclusion algorithms or Hamming distances in error-resistant transmission protocols. Previous work on HyperLTL model checking has focussed on the alternation-free fragment of HyperLTL, where verification reduces to checking a standard trace property over an appropriate self-composition of the system. The alternation-free fragment does, however, not cover general hyperliveness properties. Universal formulas, for example, cannot express the secrecy requirement that for every possible value of a secret variable there exists a computation where the value is different while the observations made by the external observer are the same. In this paper, we study the more difficult case of hyperliveness properties expressed as HyperLTL formulas with quantifier alternation. We reduce existential quantification to strategic choice and show that synthesis algorithms can be used to eliminate the existential quantifiers automatically. We furthermore show that this approach can be extended to reactive system synthesis, i.e., to automatically construct a reactive system that is guaranteed to satisfy a given HyperLTL formula.

cs.LO↗

arXiv2019

Gray-box Monitoring of Hyperproperties (Extended Version)

Many important system properties, particularly in security and privacy, cannot be verified statically. Therefore, runtime verification is an appealing alternative. Logics for hyperproperties, such as HyperLTL, support a rich set of such properties. We first show that black-box monitoring of HyperLTL is in general unfeasible, and suggest a gray-box approach. Gray-box monitoring implies performing analysis of the system at run-time, which brings new limitations to monitorabiliy (the feasibility of solving the monitoring problem). Thus, as another contribution of this paper we refine the classic notions of monitorability, both for trace properties and hyperproperties, taking into account the computability of the monitor. We then apply our approach to monitor a privacy hyperproperty called distributed data minimality, expressed as a HyperLTL property, by using an SMT-based static verifier at runtime.

cs.LO↗

arXiv2019

Runtime Verification For Timed Event Streams With Partial Information

Runtime Verification (RV) studies how to analyze execution traces of a system under observation. Stream Runtime Verification (SRV) applies stream transformations to obtain information from observed traces. Incomplete traces with information missing in gaps pose a common challenge when applying RV and SRV techniques to real-world systems as RV approaches typically require the complete trace without missing parts. This paper presents a solution to perform SRV on incomplete traces based on abstraction. We use TeSSLa as specification language for non-synchronized timed event streams and define abstract event streams representing the set of all possible traces that could have occurred during gaps in the input trace. We show how to translate a TeSSLa specification to its abstract counterpart that can propagate gaps through the transformation of the input streams and thus generate sound outputs even if the input streams contain gaps and events with imprecise values. The solution has been implemented as a set of macros for the original TeSSLa and an empirical evaluation shows the feasibility of the approach.

cs.LO↗

arXiv2019

COST Action IC 1402 ArVI: Runtime Verification Beyond Monitoring -- Activity Report of Working Group 1

This report presents the activities of the first working group of the COST Action ArVI, Runtime Verification beyond Monitoring. The report aims to provide an overview of some of the major core aspects involved in Runtime Verification. Runtime Verification is the field of research dedicated to the analysis of system executions. It is often seen as a discipline that studies how a system run satisfies or violates correctness properties. The report exposes a taxonomy of Runtime Verification (RV) presenting the terminology involved with the main concepts of the field. The report also develops the concept of instrumentation, the various ways to instrument systems, and the fundamental role of instrumentation in designing an RV framework. We also discuss how RV interplays with other verification techniques such as model-checking, deductive verification, model learning, testing, and runtime assertion checking. Finally, we propose challenges in monitoring quantitative and statistical data beyond detecting property violation.

cs.SE↗

arXiv2018

A Survey of Challenges for Runtime Verification from Advanced Application Domains (Beyond Software)

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.

cs.SE↗

arXiv2018

Timed Epistemic Knowledge Bases for Social Networks (Extended Version)

We present an epistemic logic equipped with time-stamps in the atoms and epistemic operators, which allows to reason not only about information available to the different agents, but also about the moments at which events happens and new knowledge is acquired or deduced. Our logic includes both an epistemic operator and a belief operator, which allows to model the disclosure of information that may not be accurate. Our main motivation is to model rich privacy policies in online social networks. Online Social Networks (OSNs) are increasingly used for social interactions in the modern digital era, which bring new challenges and concerns in terms of privacy. Most social networks today offer very limited mechanisms to express the desires of users in terms of how information that affects their privacy is shared. In particular, most current privacy policy formalisms allow only static policies, which are not rich enough to express timed properties like "my location after work should not be disclosed to my boss". The logic we present in this paper enables to express rich properties and policies in terms of the knowledge available to the different users and the precise time of actions and deductions. Our framework can be instantiated for different OSNs, by specifying the effect of the actions in the evolution of the social network and in the knowledge disclosed to each agent. We present an algorithm for deducing knowledge, which can also be instantiated with different variants of how the epistemic information is preserved through time. Our algorithm allows to model not only social networks with eternal information but also networks with ephemeral disclosures. Policies are modelled as formulae in the logic, which are interpreted over timed traces representing the evolution of the social network.

cs.LO↗

arXiv2014

Temporal Logics for Hyperproperties

Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.

cs.LO↗

arXiv2014

Parametrized Invariance for Infinite State Processes

We study the uniform verification problem for infinite state processes, which consists of proving that the parallel composition of an arbitrary number of processes satisfies a temporal property. Our practical motivation is to build a general framework for the temporal verification of concurrent datatypes. The contribution of this paper is a general method for the verification of safety properties of parametrized programs that manipulate complex local and global data, including mutable state in the heap. This method is based on the separation between two concerns: (1) the interaction between executing threads---handled by novel parametrized invariance rules---,and the data being manipulated---handled by specialized decision procedures. The proof rules discharge automatically a finite collection of verification conditions (VCs), the number depending only on the size of the program description and the specification, but not on the number of processes in any given instance or on the kind of data manipulated. Moreover, all VCs are quantifier free, which eases the development of decision procedures for complex data-types on top of off-the-shelf SMT solvers. We discuss the practical verification (of shape and also functional correctness properties) of a concurrent list implementation based on the method presented in this paper. Our tool also all VCs using a decision procedure for a theory of list layouts in the heap built on top of state-of-the-art SMT solvers.

cs.LO↗

arXiv2013

A Temporal Logic for Hyperproperties

Hyperproperties, as introduced by Clarkson and Schneider, characterize the correctness of a computer program as a condition on its set of computation paths. Standard temporal logics can only refer to a single path at a time, and therefore cannot express many hyperproperties of interest, including noninterference and other important properties in security and coding theory. In this paper, we investigate an extension of temporal logic with explicit path variables. We show that the quantification over paths naturally subsumes other extensions of temporal logic with operators for information flow and knowledge. The model checking problem for temporal logic with path quantification is decidable. For alternation depth 1, the complexity is PSPACE in the length of the formula and NLOGSPACE in the size of the system, as for linear-time temporal logic.

cs.LO↗

arXiv2013

A Decidable Theory of Skiplists of Unbounded Size and Arbitrary Height

This paper presents a theory of skiplists of arbitrary height, and shows decidability of the satisfiability problem for quantifier-free formulas. A skiplist is an imperative software data structure that implements sets by maintaining several levels of ordered singly-linked lists in memory, where each level is a sublist of its lower levels. Skiplists are widely used in practice because they offer a performance comparable to balanced binary trees, and can be implemented more efficiently. To achieve this performance, most implementations dynamically increment the height (the number of levels). Skiplists are difficult to reason about because of the dynamic size (number of nodes) and the sharing between the different layers. Furthermore, reasoning about dynamic height adds the challenge of dealing with arbitrary many levels. The first contribution of this paper is the theory TSL that allows to express the heap memory layout of a skiplist of arbitrary height. The second contribution is a decision procedure for the satisfiability prob- lem of quantifier-free TSL formulas. The last contribution is to illustrate the formal verification of a practical skiplist implementation using this decision procedure.

cs.LO↗