Related papers: Stack-Aware Hyperproperties
We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an…
We introduce Conflict-Aware Replicated Data Types (CARDs). CARDs are significantly more expressive than Conflict-free Replicated Data Types (CRDTs) as they support operations that can conflict with each other. Introducing conflicting…
We introduce SecRef*, a secure compilation framework protecting stateful programs verified in F* against linked unverified code, with which the program dynamically shares ML-style mutable references. To ease program verification in this…
We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information…
Distributed algorithms have many mission-critical applications ranging from embedded systems and replicated databases to cloud computing. Due to asynchronous communication, process faults, or network failures, these algorithms are difficult…
Hyperdimensional Computing (HDC) offers a computationally efficient paradigm for neuromorphic learning. Yet, it lacks rigorous uncertainty quantification, leading to open decision boundaries and, consequently, vulnerability to outliers,…
Finite-state models are ubiquitous in the study of concurrent systems, especially controllers and servers that operate in a repetitive cycle. In this paper, we show how to extract finite state models from a run of a multi-threaded Java…
We consider the model checking problem for Process Rewrite Systems (PRSs), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRSs can be adopted as formal models…
We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the…
We present a novel and well automatable approach to formal verification of C programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain evaluations. First, we reduce this problem to…
HyperLTL model-checking enables the automated verification of information-flow properties for security-critical systems. However, it only provides a binary answer. Here, we introduce two paradigms to compute counterexamples and explanations…
Graded path modalities count the number of paths satisfying a property, and generalize the existential (E) and universal (A) path modalities of CTL*. The resulting logic is called GCTL*. We settle the complexity of satisfiability of GCTL*,…
Efficient implementations of atomic objects such as concurrent stacks and queues are especially susceptible to programming errors, and necessitate automatic verification. Unfortunately their correctness criteria - linearizability with…
In logics for the strategic reasoning the main challenge is represented by their verification in contexts of imperfect information and perfect recall. In this work, we show a technique to approximate the verification of Alternating-time…
In this paper, we identify a fragment of second-order logic with restricted quantification that is expressive enough to capture numerous static analysis problems (e.g. safety proving, bug finding, termination and non-termination proving,…
Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by…
We present Hindley-Milner-Cousots (HMC), an algorithm that allows any interprocedural analysis for first-order imperative programs to be used to verify safety properties of typed higher-order functional programs. HMC works as follows.…
We introduce a set of eight universal Rules of Inference by which computer programs with known properties (axioms) are transformed into new programs with known properties (theorems). Axioms are presented to formalize a segment of Number…
When a property needs to be checked against an unknown or very complex system, classical exploration techniques like model-checking are not applicable anymore. Sometimes a~monitor can be used, that checks a given property on the underlying…
In this paper, we present a Bayesian method for statistical model checking (SMC) of probabilistic hyperproperties specified in the logic HyperPCTL* on discrete-time Markov chains (DTMCs). While SMC of HyperPCTL* using sequential probability…