| 1. |
- Algehed, Maximilian, 1995
(författare)
-
A perspective on the dependency core calculus
- 2018
-
Ingår i: Proceedings of the ACM Conference on Computer and Communications Security. - New York, NY, USA : ACM. - 1543-7221. ; , s. 24-28
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a simple but equally expressive variant on the terminating fragment of the Dependency Core Calculus (DCC) of Abadi et al. [2]. DCC is a concise and elegant calculus for tracking dependency. The calculus has applications in, among other areas, information fow control, slicing, and binding time analysis. However, in this paper we show that it is possible to replace a core technical device in DCC with an alternative, simpler, formulation. The calculus has a denotational semantics in the same domain as DCC, using which we prove that the two calculi are equivalent. As a proof of concept to show that our calculus provides a simple analysis of dependency we implement it in Haskell, obtaining a simpler implementation compared to previous work [4].
|
|
| 2. |
- Algehed, Maximilian, 1995, et al.
(författare)
-
Dynamic IFC Theorems for Free!
- 2021
-
Ingår i: 2021 IEEE 34TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2021). - : IEEE. - 2374-8303 .- 1940-1434. - 9781728176079 ; , s. 65-78
-
Konferensbidrag (refereegranskat)abstract
- We show that noninterference and transparency, the key soundness theorems for dynamic IFC libraries, can be obtained "for free", as direct consequences of the more general parametricity theorem of type abstraction. This allows us to give very short soundness proofs for dynamic IFC libraries such as faceted values and LIO. Our proofs stay short even when fully mechanized for Agda implementations of the libraries in terms of type abstraction.
|
|
| 3. |
- Algehed, Maximilian, 1995, et al.
(författare)
-
Encoding DCC in Haskell
- 2017
-
Ingår i: PLAS '17: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security. - New York, NY, USA : ACM. - 9781450350990 ; 2017-January
-
Konferensbidrag (refereegranskat)abstract
- The seminal work on the Dependency Core Calculus (DCC) shows how monads not only can be used for embedding effects in purely functional languages but also to statically track data dependencies. Such types of analysis have applications in research areas like security, partial evaluation, and slicing, where DCC plays the role of a unifying formalism. For a Haskell programmer, putting DCC into practice raises many interesting conceptual and implementation concerns. Specifically, DCC uses a non-standard bind operator, i.e., with a different type signature than that provided by monads. In fact, embedding such non-standard bind operator opens the door for many design decisions. Furthermore, it is unclear if DCC extends to traditional methods used by Haskell programmers to handle effects (such as monad transformers). In this work, we describe a novel encoding of DCC in Haskell, with a focus on its use for security—although our results also apply to the other domains. We address the concerns mentioned above and show how our implementation of DCC can be seen as a direct translation from its typing rules via the use of closed type families and type classes—two advanced type system features of Haskell. We also analyze what kind of effects DCC is compatible with and which ones it cannot secure. We also derive an alternative formulation of DCC based on fmap and a corresponding non-standard join.
|
|
| 4. |
- Algehed, Maximilian, 1995
(författare)
-
On the Foundations of Practical Language-Based Security
- 2021
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Language-based information flow control (IFC) promises to provide programming languages and tools that make it easy for developers to write secure code. Traditionally, research in this field aims to build a variant on a programming language or system that lets developers write code that gives them strong guarantees beyond the potential memory- and type-safety guarantees of modern languages. However, two developments in the field challenge this paradigm. Firstly, backwards-compatible security enforcement without false alarms promises to retrofit security enforcement on code that was not written with the enforcement mechanism in mind. This has the potential to greatly increase the applicability of IFC enforcement to legacy and mobile code from untrusted sources. Secondly, library-based security, a technique by which IFC researchers provide a software library in an established language whose programming interface gives the same guarantees as a stand-alone IFC tool for developers to use promises to do away with specialized IFC languages. This technique also has the potential to increase the applicability of IFC enforcement as developers no longer need to adopt a whole new language to get security guarantees. This thesis makes contributions to both these recent developments that come in two parts; the first part concerns enforcing secure information flow without introducing false alarms while the second part concerns the correctness of using libraries instead of fullyfledged IFC programming languages to write secure code. The first part of the thesis makes the following contributions: 1. It unifies the existing literature, in the form of Secure Multi-Execution and Multiple Facets, on security enforcement without false alarms by introducing Faceted Secure Multi-Execution. 2. It explores the unique optimisation challenges that appear in this setting. Specifically, mixing multi-execution and facets means that unnecessarily large faceted trees give rise to unnecessary executions in multi-execution and vice verse. This thesis proposes optimisation strategies that can overcome this hurdle. 3. It proves an exponential lower bound on black-box false-alarm-free enforcement and new possibility results for false-alarm-free enforcement of a variant of the noninterference security condition known as termination insensitive noninterference. 4. It classifies the special cases of enforcement that is not subject to the aforementioned exponential lower bound. Specifically, this thesis shows how and why the choice of security lattice makes the difference between exponential, polynomial, and constant overheads in multi-execution. In short, the first part of the thesis unifies the existing literature on false-alarm-free IFC enforcement and presents a number of results on the performance of enforcement mechanisms of this kind. The second part of the thesis meanwhile makes the following contributions: 1. It reduces the trusted computing base of security libraries by showing how to implement secure effects on top of an already secure core without incurring any new proof obligations. 2. It shows how to simplify DCC, the core language in the literature, without losing expressiveness. 3. It proves that noninterference can be derived in a simple and straightforward way from parametricity for both static and dynamic security libraries. This in turn reduces the conceptual gap between the kind of security libraries that are written today and the proofs one can write to prove that the libraries ensure noninterference. In short, the second part of the thesis provides a new direction for thinking about the correctness of security libraries by both reducing the amount of trusted code and by introducing improved means of proving that a security library guarantees noninterference.
|
|
| 5. |
- 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.
|
|
| 6. |
|
|
| 7. |
- 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.
|
|
| 8. |
- 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.
|
|
| 9. |
- 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.
|
|
| 10. |
- Algehed, Maximilian, 1995, et al.
(författare)
-
Transparent IFC Enforcement: Possibility and (In)Efficiency Results
- 2020
-
Ingår i: Proceedings - IEEE Computer Security Foundations Symposium. - 1940-1434. ; 2020-June, s. 65-78
-
Konferensbidrag (refereegranskat)abstract
- Information Flow Control (IFC) is a collection of techniques for ensuring a no-write-down no-read-up style security policy known as noninterference. Traditional methods for both static (e.g. type systems) and dynamic (e.g. runtime monitors) IFC suffer from untenable numbers of false alarms on real-world programs. Secure Multi-Execution (SME) promises to provide secure information flow control without modifying the behaviour of already secure programs, a property commonly referred to as transparency. Implementations of SME exist for the web in the form of the FlowFox browser and as plug-ins to several programming languages. Furthermore, SME can in theory work in a black-box manner, meaning that it can be programming language agnostic, making it perfect for securing legacy or third-party systems. As such SME, and its variants like Multiple Facets (MF) and Faceted Secure Multi-Execution (FSME), appear to be a family of panaceas for the security engineer. The question is, how come, given all these advantages, that these techniques are not ubiquitous in practice?The answer lies, partially, in the issue of runtime and memory overhead. SME and its variants are prohibitively expensive to deploy in many non-trivial situations. The natural question is why is this the case? On the surface, the reason is simple. The techniques in the SME family all rely on the idea of multi-execution, running all or parts of a program multiple times to achieve noninterference. Naturally, this causes some overhead. However, the predominant thinking in the IFC community has been that these overheads can be overcome. In this paper we argue that there are fundamental reasons to expect this not to be the case and prove two key theorems:•All transparent enforcement is polynomial time equivalent to multi-execution.•All black-box enforcement takes time exponential in the number of principals in the security lattice.Our methods also allow us to answer, in the affirmative, an open question about the possibility of secure and transparent enforcement of a security condition known as Termination Insensitive Noninterference.
|
|
| 11. |
- Algehed, Maximilian, 1995, et al.
(författare)
-
VisPar: Visualising dataflow graphs from the Par monad
- 2017
-
Ingår i: 6th ACM SIGPLAN International Workshop on Functional High-Performance Computing, FHPC 2017, Oxford, United Kingdom, 7 September 2017. - New York, NY, USA : ACM. - 9781450351812 ; , s. 24-29
-
Konferensbidrag (refereegranskat)abstract
- We present a work in progress tool (VisPar) for visualising computations in the Par monad in Haskell. Our contribution is not a revolutionary new idea but rather a modest addition to the set of tools available for making sense of parallel programs. We hope to show that VisPar can be useful as a teaching tool by providing visualisations of a few examples from a course on parallel functional programming.
|
|
| 12. |
- Bastys, Iulia, 1986, et al.
(författare)
-
SecWasm: Information Flow Control for WebAssembly
- 2022
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer Nature Switzerland. - 1611-3349 .- 0302-9743. ; 13790 LNCS, s. 74-103
-
Konferensbidrag (refereegranskat)abstract
- We introduce SecWasm, the first general purpose information-flow control system for WebAssembly (Wasm), thus extending the safety guarantees offered by Wasm with guarantees that applications manipulate sensitive data in a secure way. SecWasm is a hybrid system enforcing termination-insensitive noninterference which overcomes the challenges posed by the uncommon characteristics for machine languages of Wasm in an elegant and thorough way.
|
|
| 13. |
- Mondal, Priyanka, et al.
(författare)
-
Applying consensus and replication securely with FLAQR
- 2022
-
Ingår i: Proceedings - IEEE Computer Security Foundations Symposium. - 1940-1434. ; 2022-August, s. 163-178
-
Konferensbidrag (refereegranskat)abstract
- Availability is crucial to the security of distributed systems, but guaranteeing availability is hard, especially when participants in the system may act maliciously. Quorum replication protocols provide both integrity and availability: data and computation is replicated at multiple independent hosts, and a quorum of these hosts must agree on the output of all operations applied to the data. Unfortunately, these protocols have high overhead and can be difficult to calibrate for a specific application's needs. Ideally, developers could use high-level abstractions for consensus and replication to write fault-tolerant code by that is secure by construction. This paper presents Flow-Limited Authorization for Quorum Replication (FLAQR), a core calculus for building distributed applications with heterogeneous quorum replication protocols while enforcing end-to-end information security. Our type system ensures that well-typed FLAQR programs cannot fail (experience an unrecoverable error) in ways that violate their type-level specifications. We present noninterference theorems that characterize FLAQR's confidentiality, integrity, and availability in the presence of consensus, replication, and failures, as well as a liveness theorem for the class of majority quorum protocols under a bounded number of faults.
|
|
| 14. |
- Mondal, Priyanka, et al.
(författare)
-
Flow-limited authorization for consensus, replication, and secret sharing
- 2023
-
Ingår i: Journal of Computer Security. - 0926-227X. ; 31:5, s. 615-645
-
Tidskriftsartikel (refereegranskat)abstract
- Availability is crucial to the security of distributed systems, but guaranteeing availability is hard, especially when participants in the system may act maliciously. Quorum replication protocols provide both integrity and availability: data and computation is replicated at multiple independent hosts, and a quorum of these hosts must agree on the output of all operations applied to the data. Unfortunately, these protocols have high overhead and can be difficult to calibrate for a specific application's needs. Ideally, developers could use high-level abstractions for consensus and replication to write fault-tolerant code that is secure by construction. This paper presents Flow-Limited Authorization for Quorum Replication (FLAQR), a core calculus for building distributed applications with heterogeneous quorum replication protocols while enforcing end-to-end information security. Our type system ensures that well-typed FLAQR programs cannot fail (experience an unrecoverable error) in ways that violate their type-level specifications. We present noninterference theorems that characterize FLAQR's confidentiality, integrity, and availability in the presence of consensus, replication, and failures, as well as a liveness theorem for the class of majority quorum protocols under a bounded number of faults. Additionally, we present an extension to FLAQR that supports secret sharing as a form of declassification and prove it preserves integrity and availability security properties.
|
|
| 15. |
- Picazo-Sanchez, Pablo, 1985, et al.
(författare)
-
DeDup.js: Discovering Malicious and Vulnerable Extensions by Detecting Duplication
- 2022
-
Ingår i: PROCEEDINGS OF THE 8TH INTERNATIONAL CONFERENCE ON INFORMATION SYSTEMS SECURITY AND PRIVACY (ICISSP). - : SCITEPRESS - Science and Technology Publications. - 9789897585531 ; 1, s. 528-535
-
Konferensbidrag (refereegranskat)abstract
- Browser extensions are popular web applications that users install in modern browsers to enrich the user experience on the web. It is common for browser extensions to include static resources in the form of HTML, CSS, fonts, images, and JavaScript libraries. Unfortunately, the state of the art is that each extension ships its own version of a given resource. This paper presents DeDup.js, a framework that incorporates similarity analysis for achieving two goals: detecting potentially malicious extensions during the approval process, and given an extension as input, DeDup.js discovers similar extensions. We downloaded three snapshots of the Google Chrome Web Store during one year totaling more than 422k browser extensions and conclude that over 50% of the static resources are shared among the extensions. By implementing an instance of DeDup.js, we detect more than 7k extensions that should not have been published and were later deleted. Also, we discover more than 1k malicious extensions still online that send user's queries to external servers without the user's knowledge. Finally, we show the potential of DeDup.js by analyzing a set extensions part of CacheFlow, a recently discovered attack. We detect 53 malicious extensions of which 36 Google has already taken down and the rest are investigated.
|
|
| 16. |
- Schmitz, Thomas, et al.
(författare)
-
Faceted secure multi execution
- 2018
-
Ingår i: Proceedings of the ACM Conference on Computer and Communications Security. - New York, NY, USA : ACM. - 1543-7221. ; , s. 1617-1634
-
Konferensbidrag (refereegranskat)abstract
- Publication rights licensed to ACM. To enforce non-interference, both Secure Multi-Execution (SME) and Multiple Facets (MF) rely on the introduction of multi-executions. The attractiveness of these techniques is that they are precise: secure programs running under SME or MF do not change their behavior. Although MF was intended as an optimization for SME, it does provide a weaker security guarantee for termination leaks. This paper presents Faceted Secure Multi Execution (FSME), a novel synthesis of MF and SME that combines the stronger security guarantees of SME with the optimizations of MF. The development of FSME required a unification of the ideas underlying MF and SME into a new multi-execution framework (), which can be parameterized to provide MF, SME, or our new approach FSME, thus enabling an apples-to-apples comparison and benchmarking of all three approaches. Unlike the original work on MF and SME, supports arbitrary (and possibly infinite) lattices necessary for decentralized labeling models—a feature needed in order to make possible the writing of applications where each principal can impose confidentiality and integrity requirements on data. We provide some micro-benchmarks for evaluating and write a file hosting service, called ProtectedBox, whose functionality can be securely extended via third-party plugins.
|
|
| 17. |
- Smallbone, Nicholas, 1986, et al.
(författare)
-
Quick Specifications for the Busy Programmer
- 2017
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 27
-
Tidskriftsartikel (refereegranskat)abstract
- QuickSpec is a theory exploration system which tests a Haskell program to find equational properties of it, automatically. The equations can be used to help understand the program, or as lemmas to help prove the program correct. QuickSpec is largely automatic: the user just supplies the functions to be tested and QuickCheck data generators.Previous theory exploration systems, including earlier versions of QuickSpec itself, scaled poorly. This paper describes a new architecture for theory exploration with which we can find vastly more complex laws than before, and much faster. We demonstrate theory exploration in QuickSpec on problems both from functional programming and mathematics.
|
|
