| 1. |
- Algehed, Maximilian, 1995, et al.
(författare)
-
Optimising Faceted Secure Multi-Execution
- 2019
-
Ingår i: Proceedings - IEEE Computer Security Foundations Symposium. - 1940-1434. ; 2019-June, s. 1-16
-
Konferensbidrag (refereegranskat)abstract
- Language-Based Information Flow Control (IFC) provides strong security guarantees for untrusted code, but often suffers from a non-negligible rate of false alarms. Multi-execution based techniques promise to provide security guarantees without raising any false alarms. However, all known multi-execution approaches introduce extraneous performance overheads which are rarely studied. In this work, we lay down the foundations for optimisation techniques aimed at reducing these overheads to a managable level, thus helping to make multi-execution more practical. We characterise our optimisations as data-and control-oriented. Data-oriented optimisations reduce storage overheads- which also helps to remove unnecessary repeated computations. In contrast, computation-oriented optimisations rely on program annotations in order to reduce needless computation. These annotations motivate the need for a new, stronger, theoretical notion of transparency- i.e., a stronger notion for characterising the lack of false alarms. To show the efficacy of our optimisation techniques, we apply them to two case-studies: a secure (faceted) database and a chat server written in a multi-execution based IFC framework. Our case-studies clearly show that our optimisations significantly reduce the storage and computational overhead, sometimes from exponential to polynomial order. All of our formal results are accompanied by mechanised proofs in Agda.
|
|
| 2. |
- Algehed, Maximilian, 1995, et al.
(författare)
-
Saint: an API-generic type-safe interpreter
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11457 LNCS, s. 94-113
-
Konferensbidrag (refereegranskat)abstract
- Many programs written in the functional programming language Haskell take advantage of its advanced type system. Haskell's type system is very expressive and allows us to write interesting programs without sacrificing type safety. Haskell programs that expose its API to an open world, however, are faced with the problem of dynamic type checking. Existing techniques that address this problem, such as Typeable and Dynamic, are often closed and difficult to extend. We have constructed an extensible library for describing APIs using annotated type representations. As a result, API calls can be interpreted in a type-safe manner without any extra programming effort. In addition, the user has full control over the universe of allowed types, which helps to catch any misconceptions in an early stage. We have applied our technique to connect a real-world DSL (GRACe) to a JavaScript GUI.
|
|
| 3. |
- Algehed, Maximilian, 1995
(författare)
-
Securing the Foundations of Practical Information Flow Control
- 2019
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Language-based information flow control (IFC) promises to secure computer programs against malicious or incompetent programmers by addressing key shortcomings of modern programming languages. In spite of showing great promise, the field remains under-utilised in practise. This thesis makes contributions to the theoretical foundations of IFC aimed at making the techniques practically applicable. The paper addresses two primary topics, IFC as a library and IFC without false alarms. The contributions range from foundational observations about soundness and completeness, to practical considerations of efficiency and expressiveness.
|
|
| 4. |
- Algehed, Maximilian, 1995, et al.
(författare)
-
Simple Noninterference from Parametricity
- 2019
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 3
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper we revisit the connection between parametricity and noninterference. Our primary contribution is a proof of noninterference for a polyvariant variation of the Dependency Core Calculus of in the Calculus of Constructions. The proof is modular: it leverages parametricity for the Calculus of Constructions and the encoding of data abstraction using existential types. This perspective gives rise to simple and understandable proofs of noninterference from parametricity. All our contributions have been mechanised in the Agda proof assistant.
|
|
