| 1. |
- Cambronero, Maria Emilia, 1978, et al.
(författare)
-
Towards a GDPR-compliant cloud architecture with data privacy controlled through sticky policies
- 2024
-
Ingår i: PeerJ Computer Science. ; 10
-
Tidskriftsartikel (refereegranskat)abstract
- Data privacy is one of the biggest challenges facing system architects at the system design stage. Especially when certain laws, such as the General Data Protection Regulation (GDPR), have to be complied with by cloud environments. In this article, we want to help cloud providers comply with the GDPR by proposing a GDPR-compliant cloud architecture. To do this, we use model-driven engineering techniques to design cloud architecture and analyze cloud interactions. In particular, we develop a complete framework, called MDCT, which includes a Unified Modeling Language profile that allows us to define specific cloud scenarios and profile validation to ensure that certain required properties are met. The validation process is implemented through the Object Constraint Language (OCL) rules, which allow us to describe the constraints in these models. To comply with many GDPR articles, the proposed cloud architecture considers data privacy and data tracking, enabling safe and secure data management and tracking in the context of the cloud. For this purpose, sticky policies associated with the data are incorporated to define permission for third parties to access the data and track instances of data access. As a result, a cloud architecture designed with MDCT contains a set of OCL rules to validate it as a GDPR-compliant cloud architecture. Our tool models key GDPR points such as user consent/withdrawal, the purpose of access, and data transparency and auditing, and considers data privacy and data tracking with the help of sticky policies.
|
|
| 2. |
- 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.
|
|
| 3. |
- 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.
|
|
| 4. |
- 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.
|
|
| 5. |
- Barthe, Gilles, et al.
(författare)
-
Security of Multithreaded Programs by Compilation
- 2007
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. - 9783540748342 ; 4734, s. 2-18
-
Konferensbidrag (refereegranskat)
|
|
| 6. |
- 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.
|
|
| 7. |
- Bello, Luciano, 1981, et al.
(författare)
-
Towards a Taint Mode for Cloud Computing Web Application
- 2012
-
Ingår i: 7th Workshop on Programming Languages and Analysis for Security. - New York, NY, USA : ACM. - 9781450314411 ; , s. 7:1--7:12-
-
Konferensbidrag (refereegranskat)abstract
- Cloud computing is generally understood as the distribution of data and computations over the Internet. Over the past years, there has been a steep increase in web sites using this technology. Unfortunately, those web sites are not exempted from injection flaws and cross-site scripting, two of the most common security risks in web applications. Taint analysis is an automatic approach to detect vulnerabilities. Cloud computing platforms possess several features that, while facilitating the development of web applications, make it difficult to apply off-the-shelf taint analysis techniques. More specifically, several of the existing taint analysis techniques do not deal with persistent storage (e.g. object datastores), opaque objects (objects whose implementation cannot be accessed and thus tracking tainted data becomes a challenge), or a rich set of security policies (e.g. forcing a specific order of sanitizers to be applied). We propose a taint analysis for could computing web applications that consider these aspects. Rather than modifying interpreters or compilers, we provide taint analysis via a Python library for the cloud computing platform Google App Engine (GAE). To evaluate the use of our library, we harden an existing GAE web application against cross-site scripting attacks.
|
|
| 8. |
- Benitez, Sergio, et al.
(författare)
-
Short Paper: Blockcheck the Typechain
- 2020
-
Ingår i: PLAS 2020 - Proceedings of the 15th Workshop on Programming Languages and Analysis for Security. - New York, NY, USA : ACM. ; 13 November 2020, s. 35-39
-
Konferensbidrag (refereegranskat)abstract
- Recent efforts have sought to design new smart contract programming languages that make writing blockchain programs safer. But programs on the blockchain are beholden only to the safety properties enforced by the blockchain itself: even the strictest language-only properties can be rendered moot on a language-oblivious blockchain due to inter-contract interactions. Consequently, while safer languages are a necessity, fully realizing their benefits necessitates a language-aware redesign of the blockchain itself. To this end, we propose that the blockchain be viewed as a typechain: a chain of typed programs-not arbitrary blocks-that are included iff they typecheck against the existing chain. Reaching consensus, or blockchecking, validates typechecking in a byzantine fault-tolerant manner. Safety properties traditionally enforced by a runtime are instead enforced by a type system with the aim of statically capturing smart contract correctness. To provide a robust level of safety, we contend that a typechain must minimally guarantee (1) asset linearity and liveness, (2) physical resource availability, including CPU and memory, (3) exceptionless execution, or no early termination, (4) protocol conformance, or adherence to some state machine, and (5) inter-contract safety, including reentrancy safety. Despite their exacting nature, typechains are extensible, allowing for rich libraries that extend the set of verified properties. We expand on typechain properties and present examples of real-world bugs they prevent.
|
|
| 9. |
- Birgisson, Arnar, 1981, et al.
(författare)
-
Capabilities for information flow
- 2011
-
Ingår i: ACM SIGPLAN Workshop on Programming Languages and Analysis for Security. - New York, NY, USA : ACM. - 9781450308304 ; , s. article no. 5-
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a capability-based mechanism for permissiveyet secure enforcement of information-flow policies. Language capabilities have been studied widely, and several popular implementations, such as Caja and Joe-E, are available. By making the connection from capabilities to information flow, we enable smoothenforcement of information-flow policies using capability systems.The paper presents a transformation that given an arbitrary source program in a simple imperative language produces a secure program in a language with capabilities. We present formal guarantees of security and permissiveness and report on experiments to enforce information-flow policies for web applications using Caja.
|
|
| 10. |
- 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.
|
|
