Skip to main content
main-content

Über dieses Buch

This open access book constitutes the proceedings of the 8th International Conference on Principles of Security and Trust, POST 2019, which took place in Prague, Czech Republic, in April 2019, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2019.

The 10 papers presented in this volume were carefully reviewed and selected from 27 submissions. They deal with theoretical and foundational aspects of security and trust, including on new theoretical results, practical applications of existing foundational ideas, and innovative approaches stimulated by pressing practical problems.

Inhaltsverzeichnis

Frontmatter

Open Access

Foundations for Parallel Information Flow Control Runtime Systems

Abstract
We present the foundations for a new dynamic information flow control (IFC) parallel runtime system, LIO\(_{\mathrm {PAR}}\). To our knowledge, LIO\(_{\mathrm {PAR}}\) is the first dynamic language-level IFC system to (1) support deterministic parallel thread execution and (2) eliminate both internal- and external-timing covert channels that exploit the runtime system. Most existing IFC systems are vulnerable to external timing attacks because they are built atop vanilla runtime systems that do not account for security—these runtime systems allocate and reclaim shared resources (e.g., CPU-time and memory) fairly between threads at different security levels. While such attacks have largely been ignored—or, at best, mitigated—we demonstrate that extending IFC systems with parallelism leads to the internalization of these attacks. Our IFC runtime system design addresses these concerns by hierarchically managing resources—both CPU-time and memory—and making resource allocation and reclamation explicit at the language-level. We prove that LIO\(_{\mathrm {PAR}}\) is secure, i.e., it satisfies progress- and timing-sensitive non-interference, even when exposing clock and heap-statistics APIs.
Marco Vassena, Gary Soeller, Peter Amidon, Matthew Chan, John Renner, Deian Stefan

Open Access

A Formal Analysis of Timing Channel Security via Bucketing

Abstract
This paper investigates the effect of bucketing in security against timing channel attacks. Bucketing is a technique proposed to mitigate timing-channel attacks by restricting a system’s outputs to only occur at designated time intervals, and has the effect of reducing the possible timing-channel observations to a small number of possibilities. However, there is little formal analysis on when and to what degree bucketing is effective against timing-channel attacks. In this paper, we show that bucketing is in general insufficient to ensure security. Then, we present two conditions that can be used to ensure security of systems against adaptive timing channel attacks. The first is a general condition that ensures that the security of a system decreases only by a limited degree by allowing timing-channel observations, whereas the second condition ensures that the system would satisfy the first condition when bucketing is applied and hence becomes secure against timing-channel attacks. A main benefit of the conditions is that they allow separation of concerns whereby the security of the regular channel can be proven independently of concerns of side-channel information leakage, and certain conditions are placed on the side channel to guarantee the security of the whole system. Further, we show that the bucketing technique can be applied compositionally in conjunction with the constant-time-implementation technique to increase their applicability. While we instantiate our contributions to timing channel and bucketing, many of the results are actually quite general and are applicable to any side channels and techniques that reduce the number of possible observations on the channel.
Tachio Terauchi, Timos Antonopoulos

Open Access

A Dependently Typed Library for Static Information-Flow Control in Idris

Abstract
Safely integrating third-party code in applications while protecting the confidentiality of information is a long-standing problem. Pure functional programming languages, like Haskell, make it possible to enforce lightweight information-flow control through libraries like MAC by Russo. This work presents DepSec, a MAC inspired, dependently typed library for static information-flow control in Idris. We showcase how adding dependent types increases the expressiveness of state-of-the-art static information-flow control libraries and how DepSec matches a special-purpose dependent information-flow type system on a key example. Finally, we show novel and powerful means of specifying statically enforced declassification policies using dependent types.
Simon Gregersen, Søren Eller Thomsen, Aslan Askarov

Open Access

Achieving Safety Incrementally with Checked C

Abstract
Checked C is a new effort working toward a memory-safe C. Its design is distinguished from that of prior efforts by truly being an extension of C: Every C program is also a Checked C program. Thus, one may make incremental safety improvements to existing codebases while retaining backward compatibility. This paper makes two contributions. First, to help developers convert existing C code to use so-called checked (i.e., safe) pointers, we have developed a preliminary, automated porting tool. Notably, this tool takes advantage of the flexibility of Checked C’s design: The tool need not perfectly classify every pointer, as required of prior all-or-nothing efforts. Rather, it can make a best effort to convert more pointers accurately, without letting inaccuracies inhibit compilation. However, such partial conversion raises the question: If safety violations can still occur, what sort of advantage does using Checked C provide? We draw inspiration from research on migratory typing to make our second contribution: We prove a blame property that renders so-called checked regions blameless of any run-time failure. We formalize this property for a core calculus and mechanize the proof in Coq.
Andrew Ruef, Leonidas Lampropoulos, Ian Sweet, David Tarditi, Michael Hicks

Open Access

: A DSL for Verified Secure Multi-party Computations

Abstract
Secure multi-party computation (MPC) enables a set of mutually distrusting parties to cooperatively compute, using a cryptographic protocol, a function over their private data. This paper presents \(\textsc {Wys}^\star \), a new domain-specific language (DSL) for writing mixed-mode MPCs. \(\textsc {Wys}^\star \) is an embedded DSL hosted in F\(^\star \), a verification-oriented, effectful programming language. \(\textsc {Wys}^\star \) source programs are essentially F\(^\star \) programs written in a custom MPC effect, meaning that the programmers can use F\(^\star \)’s logic to verify the correctness and security properties of their programs. To reason about the distributed runtime semantics of these programs, we formalize a deep embedding of \(\textsc {Wys}^\star \), also in F\(^\star \). We mechanize the necessary metatheory to prove that the properties verified for the \(\textsc {Wys}^\star \) source programs carry over to the distributed, multi-party semantics. Finally, we use F\(^\star \)’s extraction to extract an interpreter that we have proved matches this semantics, yielding a partially verified implementation. \(\textsc {Wys}^\star \) is the first DSL to enable formal verification of MPC programs. We have implemented several MPC protocols in \(\textsc {Wys}^\star \), including private set intersection, joint median, and an MPC-based card dealing application, and have verified their correctness and security.
Aseem Rastogi, Nikhil Swamy, Michael Hicks

Open Access

Generalised Differential Privacy for Text Document Processing

Abstract
We address the problem of how to “obfuscate” texts by removing stylistic clues which can identify authorship, whilst preserving (as much as possible) the content of the text. In this paper we combine ideas from “generalised differential privacy” and machine learning techniques for text processing to model privacy for text documents. We define a privacy mechanism that operates at the level of text documents represented as “bags-of-words”—these representations are typical in machine learning and contain sufficient information to carry out many kinds of classification tasks including topic identification and authorship attribution (of the original documents). We show that our mechanism satisfies privacy with respect to a metric for semantic similarity, thereby providing a balance between utility, defined by the semantic content of texts, with the obfuscation of stylistic clues. We demonstrate our implementation on a “fan fiction” dataset, confirming that it is indeed possible to disguise writing style effectively whilst preserving enough information and variation for accurate content classification tasks. We refer the reader to our complete paper [15] which contains full proofs and further experimentation details.
Natasha Fernandes, Mark Dras, Annabelle McIver

Open Access

Symbolic Verification of Distance Bounding Protocols

Abstract
With the proliferation of contactless applications, obtaining reliable information about distance is becoming an important security goal, and specific protocols have been designed for that purpose. These protocols typically measure the round trip time of messages and use this information to infer a distance. Formal methods have proved their usefulness when analysing standard security protocols such as confidentiality or authentication protocols. However, due to their abstract communication model, existing results and tools do not apply to distance bounding protocols.
In this paper, we consider a symbolic model suitable to analyse distance bounding protocols, and we propose a new procedure for analysing (a bounded number of sessions of) protocols in this model. The procedure has been integrated in the Akiss tool and tested on various distance bounding and payment protocols (e.g. MasterCard, NXP).
Alexandre Debant, Stéphanie Delaune

Open Access

On the Formalisation of -Protocols and Commitment Schemes

Abstract
There is a fundamental relationship between \(\varSigma \)-protocols and commitment schemes whereby the former can be used to construct the latter. In this work we provide the first formal analysis in a proof assistant of such a relationship and in doing so formalise \(\varSigma \)-protocols and commitment schemes and provide proofs of security for well known instantiations of both primitives.
Every definition and every theorem presented in this paper has been checked mechanically by the Isabelle/HOL proof assistant.
David Butler, David Aspinall, Adrià Gascón

Open Access

Orchestrating Layered Attestations

Abstract
We present Copland, a language for specifying layered attestations. Layered attestations provide a remote appraiser with structured evidence of the integrity of a target system to support a trust decision. The language is designed to bridge the gap between formal analysis of attestation security guarantees and concrete implementations. We therefore provide two semantic interpretations of terms in our language. The first is a denotational semantics in terms of partially ordered sets of events. This directly connects Copland to prior work on layered attestation. The second is an operational semantics detailing how the data and control flow are executed. This gives explicit implementation guidance for attestation frameworks. We show a formal connection between the two semantics ensuring that any execution according to the operational semantics is consistent with the denotational event semantics. This ensures that formal guarantees resulting from analyzing the event semantics will hold for executions respecting the operational semantics. All results have been formally verified with the Coq proof assistant.
John D. Ramsdell, Paul D. Rowe, Perry Alexander, Sarah C. Helble, Peter Loscocco, J. Aaron Pendergrass, Adam Petz

Open Access

Verifying Liquidity of Bitcoin Contracts

Abstract
A landmark security property of smart contracts is liquidity: in a non-liquid contract, it may happen that some funds remain frozen. The relevance of this issue is witnessed by a recent liquidity attack to the Ethereum Parity Wallet, which has frozen \({\sim }160M\) USD within the contract, making this sum unredeemable by any user. We address the problem of verifying liquidity of Bitcoin contracts. Focussing on BitML, a contracts DSL with a computationally sound compiler to Bitcoin, we study various notions of liquidity. Our main result is that liquidity of BitML contracts is decidable, in all the proposed variants. To prove this, we first transform the infinite-state semantics of BitML into a finite-state one, which focusses on the behaviour of any given set of contracts, abstracting the context moves. With respect to the chosen contracts, this abstraction is sound and complete. Our decision procedure for liquidity is then based on model-checking the finite space of states of the abstraction.
Massimo Bartoletti, Roberto Zunino

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise