| 1. |
- Birgisson, Arnar, 1981, et al.
(författare)
-
Unifying Facets of Information Integrity
- 2010
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642177132 ; 6503, s. 48-65
-
Konferensbidrag (refereegranskat)abstract
- Information integrity is a vital security property in a variety of applications. However, there is more than one facet to integrity: interpretations of integrity in different contexts include integrity via information flow, where the key is that trusted output is independent from untrusted input, and integrity via invariance, where the key is preservation of an invariant. Furthermore, integrity via invariance is itself multi-faceted. For example, the literature features formalizations of invariance as predicate preservation (predicate invariance), which is not directly compatible with invariance of memory values (value invariance).This paper offers a unified framework for integrity policies that include all of the facets above. Despite the different nature of these facets, we show that a straightforward enforcement mechanism adapted from the literature is readily available for enforcing all of the integrity facets at once.
|
|
| 2. |
- Barthe, Gilles, et al.
(författare)
-
Secuirty of Multithreaded Programs by Compilation
- 2009
-
Ingår i: Special Issue of ACM Transactions on Information and System Security (TISSEC). - : Association for Computing Machinery (ACM). - 1094-9224 .- 1557-7406.
-
Tidskriftsartikel (refereegranskat)abstract
- Information security is a pressing challenge for mobile code technologies. In order to claim end-to-end security of mobile code, it is necessary to establish that the code neither intentionally nor accidentally propagates sensitive information to an adversary. Although mobile code is commonly multithreaded low-level code, the literature is lacking enforcement mechanisms that ensure information security for such programs.This article offers a modular solution to the security ofmultithreaded programs. The modularity is three-fold:we give modular extensions of sequential semantics, sequential security typing, and sequential security-type preserving compilation that allow us enforcing security for multithreaded programs. Thanks to the modularity, there are no more restrictions on multithreaded source programs than on sequential ones, and yet we guarantee that their compilations are provably secure for a wide class of schedulers.
|
|
| 3. |
- Barthes, Gilles, et al.
(författare)
-
Security of Multithreaded Programs by Compilation
- 2010
-
Ingår i: ACM Transactions on Information and System Security. - 1094-9224. ; 13:3
-
Tidskriftsartikel (refereegranskat)abstract
- End-to-End security of mobile code requires that the code neither intentionally nor accidentally propagates sensitive information to an adversary. Although mobile code is commonly multithreaded low-level code, there lack enforcement mechanisms that ensure information security for such programs. The modularity is three-fold: we give modular extensions of sequential semantics, sequential security typing, and sequential security-type preserving compilation that allow us enforcing security for multithreaded programs. Thanks to the modularity, there are no more restrictions on multithreaded source programs than on sequential ones, and yet we guarantee that their compilations are provably secure for a wide class of schedulers.
|
|
| 4. |
- Vassena, Marco, 1991, et al.
(författare)
-
Flexible manipulation of labeled values for information-flow control libraries
- 2016
-
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. - 9783319457437 ; 9878 LNCS, 2016, s. 538-557
-
Konferensbidrag (refereegranskat)abstract
- The programming language Haskell plays a unique, privileged role in Information-Flow Control (IFC) research: it is able to enforce information security via libraries. Many state-of-the-art libraries (e.g., LIO, HLIO, and MAC) allow computations to manipulate data with different security labels by introducing the notion of labeled values, which protect values with explicit labels by means of an abstract data type. While computations have an underlying algebraic structure in such libraries (i.e. monads), there is no research on structures for labeled values and their impact on the programming model. In this paper, we add the functor structure to labeled values, which allows programmers to conveniently and securely perform computations without side-effects on such values, and an applicative operator, which extends this feature to work on multiple labeled values combined by a multi-parameter function. This functionality simplifies code, as it does not force programmers to spawn threads to manipulate sensitive data with side-effect free operations. Additionally, we present a relabel primitive which securely modifies the label of labeled values. This operation also helps to simplify code when aggregating data with heterogeneous labels, as it does not require spawning threads to do so. We provide mechanized proofs of the soundness our contributions for the security library MAC, although we remark that our ideas apply to LIO and HLIO as well.
|
|
| 5. |
- Vassena, Marco, 1991, et al.
(författare)
-
MAC A verified static information-flow control library
- 2018
-
Ingår i: Journal of Logical and Algebraic Methods in Programming. - : Elsevier BV. - 2352-2208 .- 2352-2216. ; 95, s. 148-180
-
Tidskriftsartikel (refereegranskat)abstract
- The programming language Haskell plays a unique, privileged role in information-flow control (IFC) research: it is able to enforce information security via libraries. Many state-of-the-art IFC libraries (e.g., LIO and HLIO) support a variety of advanced features like mutable data structures, exceptions, and concurrency, whose subtle interaction makes verification of security guarantees challenging. In this work, we focus on MAC, a statically-enforced IFC library for Haskell. In MAC, like other IFC libraries, computations have a well-established algebraic structure for computations (i.e., monads) responsible to manipulate labeled values values coming from an abstract data type which associates a sensitivity label to a piece of information. In this work, we enrich labeled values with a functor structure and provide an applicative functor operator which encourages a more functional programming style and simplifies code. Furthermore, we present a full-fledged, mechanically-verified model of MAC. Specifically, we show progress-insensitive noninterference for our sequential calculus and pinpoint sufficient requirements on the scheduler to prove progress-sensitive noninterference for our concurrent calculus. For that, we study the security guarantees of MAC using term erasure, a proof technique that ensures that the same public output should be produced if secrets are erased before or after program execution. As another contribution, we extend term erasure with two-steps erasure, a flexible novel technique that greatly simplifies the noninterference proof and helps to prove many advanced features of MAC.
|
|
