Unifying theories distil common features of programming languages and design methods by means of algebraic operators and their laws. Several practical concerns---e.g., improvement of a program, conformance of code with design, correctness with respect to specified requirements---are subsumed by the beautiful notion that programs and designs are special forms of specification and their relationships are instances of logical implication between specifications. Mathematical development of this idea has been very successful but limited to an impoverished notion of specification: trace properties. Some mathematically precise properties of programs---dubbed hyperproperties---refer to traces collectively. For example, confidentiality involves knowledge of possible traces. This article reports on both obvious and surprising results about lifting algebras of programming to hyperproperties, especially in connection with loops, and suggests directions for further research. The main results are: the first compositional semantics of imperative programs with loops, at the hyper level, and a proof that this semantics is the same as the direct image of a standard semantics, for subset closed hyperproperties.
Epistemic logic is the topic of a textbook @cite_22 and has been explored in the security literature @cite_21 . Mantel considers a range of security properties via closure operators @cite_33 . The limited usefulness of trace refinement for proving @math even for deterministic programs, as in the chain ), is discussed by Assaf and Pasqua @cite_24 @cite_29 . The formulation of possibilistic noninterference as @math is due to Joshi and Leino @cite_27 and resembles the formulation of @cite_5 .
@cite_22 @cite_33 @cite_29 @cite_21 @cite_24 @cite_27 @cite_5
2097744609 2889050595 2097365905 2509308157 2173102238
When complex systems are constructed from simpler components it is important to know how properties of the components behave under composition. We present various compositionality results for security properties. In particular we introduce a novel security property and show that this property is, in general, composable although it is weaker than forward correctability. Moreover we demonstrate that certain nontrivial security properties emerge under composition and illustrate how this fact can be exploited. All compositionality results that we present are verified with the help of a single, quite powerful lemma. Basing on this lemma, we also re-prove several already known compositionality results with the objective to unify these results. As a side effect, we obtain a classification of known compositionality results for security properties. Hyperproperties are quickly becoming very popular in the context of systems security, due to their expressive power. They differ from classic trace properties since they are represented by sets of sets of executions instead of sets of executions. This allows us, for instance, to capture information flow security specifications, which cannot be expressed as trace properties, namely as predicates over single executions. In this work, we reason about how it is possible to move standard abstract interpretation-based static analysis methods, designed for trace properties, towards the verification of hyperproperties. In particular, we focus on the verification of bounded subset-closed hyperproperties which are easier to verify than generic hyperproperties. It turns out that a lot of interesting specifications (e.g., Non-Interference) lie in this category. Temporal epistemic logic is a well-established framework for expressing agents knowledge and how it evolves over time. Within language-based security these are central issues, for instance in the context of declassification. We propose to bring these two areas together. The paper presents a computational model and an epistemic temporal logic used to reason about knowledge acquired by observing program outputs. This approach is shown to elegantly capture standard notions of noninterference and declassification in the literature as well as information flow properties where sensitive and public data intermingle in delicate ways. We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Galois connection that directly approximates the hyperproperty of interest. To enable use of such Galois connections, we introduce a fixpoint characterisation of hypercollecting semantics, i.e. a â set of sets" transformer. This makes it possible to systematically derive static analyses for hyperproperties entirely within the calculational framework of abstract interpretation. We evaluate this technique by deriving example static analyses. For qualitative information flow, we derive a dependence analysis similar to the logic of Amtoft and Banerjee (SASâ 04) and the type system of Hunt and Sands (POPLâ 06). For quantitative information flow, we derive a novel cardinality analysis that bounds the leakage conveyed by a program instead of simply deciding whether it exists. This encompasses problems that are hypersafety but not k-safety. We put the framework to use and introduce variations that achieve precision rivalling the most recent and precise static analyses for information flow. A classic problem in security is to determine whether a program has secure information flow. Informally, this problem is described as follows: Given a program with variables partitioned into two disjoint sets of “high-security” and “low-security” variables, check whether observations of the low-security variables reveal any information about the initial values of the high-security variables. Although the problem has been studied for several decades, most previous approaches have been syntactic in nature, often using type systems and compiler data flow analysis techniques to analyze program texts. This paper presents a considerably different approach to checking secure information flow, based on a semantic characterization. A semantic approach has several desirable features. Firstly, it gives a more precise characterization of security than that provided by most previous approaches. Secondly, it applies to any programming constructs whose semantics are definable; for instance, the introduction of nondeterminism and exceptions poses no additional problems. Thirdly, it can be used for reasoning about indirect leaking of information through variations in program behavior (e.g., whether or not the program terminates).