-
Information-flow Interfaces and Security Lattices
Authors:
Ezio Bartocci,
Thomas A. Henzinger,
Dejan Nickovic,
Ana Oliveira da Costa
Abstract:
Information-flow interfaces is a formalism recently proposed for specifying, composing, and refining system-wide security requirements. In this work, we show how the widely used concept of security lattices provides a natural semantic interpretation for information-flow interfaces.
Information-flow interfaces is a formalism recently proposed for specifying, composing, and refining system-wide security requirements. In this work, we show how the widely used concept of security lattices provides a natural semantic interpretation for information-flow interfaces.
△ Less
Submitted 20 June, 2024;
originally announced June 2024.
-
Hypernode Automata
Authors:
Ezio Bartocci,
Thomas A. Henzinger,
Dejan Nickovic,
Ana Oliveira da Costa
Abstract:
We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on ex…
▽ More
We introduce hypernode automata as a new specification formalism for hyperproperties of concurrent systems. They are finite automata with nodes labeled with hypernode logic formulas and transitions labeled with actions. A hypernode logic formula specifies relations between sequences of variable values in different system executions. Unlike HyperLTL, hypernode logic takes an asynchronous view on execution traces by constraining the values and the order of value changes of each variable without correlating the timing of the changes. Different execution traces are synchronized solely through the transitions of hypernode automata. Hypernode automata naturally combine asynchronicity at the node level with synchronicity at the transition level. We show that the model-checking problem for hypernode automata is decidable over action-labeled Kripke structures, whose actions induce transitions of the specification automaton. For this reason, hypernode automaton is a suitable formalism for specifying and verifying asynchronous hyperproperties, such as declassifying observational determinism in multi-threaded programs.
△ Less
Submitted 8 January, 2024; v1 submitted 4 May, 2023;
originally announced May 2023.
-
Flavours of Sequential Information Flow
Authors:
Ezio Bartocci,
Thomas Ferrère,
Thomas A. Henzinger,
Dejan Nickovic,
Ana Oliveira da Costa
Abstract:
Information-flow policies prescribe which information is available to a given user or subsystem. We study the problem of specifying such properties in reactive systems, which may require dynamic changes in information-flow restrictions between their states. We formalize several flavours of sequential information-flow, which cover different assumptions about the semantic relation between multiple o…
▽ More
Information-flow policies prescribe which information is available to a given user or subsystem. We study the problem of specifying such properties in reactive systems, which may require dynamic changes in information-flow restrictions between their states. We formalize several flavours of sequential information-flow, which cover different assumptions about the semantic relation between multiple observations of a system. Information-flow specification falls into the category of hyperproperties. We define different variants of sequential information-flow specification using a first-order logic with both trace quantifiers and temporal quantifiers called Hypertrace Logic. We prove that HyperLTL, equivalent to a subset of Hypertrace Logic with restricted quantifier prefixes, cannot specify the majority of the studied two-state independence variants. For our results, we introduce a notion of equivalence between sets of traces that cannot be distinguished by certain classes of formulas in Hypertrace Logic. This presents a new approach to proving inexpressiveness results for logics such as HyperLTL.
△ Less
Submitted 5 May, 2021;
originally announced May 2021.
-
Information-Flow Interfaces
Authors:
Ezio Bartocci,
Thomas Ferrère,
Thomas A. Henzinger,
Dejan Nickovic,
Ana Oliveira da Costa
Abstract:
Contract-based design is a promising methodology for taming the complexity of develo** sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory…
▽ More
Contract-based design is a promising methodology for taming the complexity of develo** sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees. Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory that is designed for ensuring system-wide security properties, thus paving the way for a science of safety and security co-engineering. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. We illustrate the applicability of our framework with an example inspired from the automotive domain. Finally, we provide three plausible trace semantics to stateful information-flow interfaces and we show that only two correspond to temporal logics for specifying hyperproperties, while the third defines a new class of hyperproperties that lies between the other two classes.
△ Less
Submitted 7 May, 2020; v1 submitted 15 February, 2020;
originally announced February 2020.
