| 1. |
- Agat, J., et al.
(författare)
-
On Confidentiality and Algorithms
- 2001
-
Ingår i: Proceedings of the 2001 IEEE Symposium on Security and Privacy (S&P-01) / Titsworth, Francis M.. ; , s. 64-77
-
Konferensbidrag (refereegranskat)abstract
- Recent interest in methods for certifying programs for secureinformation flow (noninterference) have failed to raise a key question: can efficient algorithmsbe written so as to satisfy the requirements of secure information flow? In this paper we discuss how algorithms for searching and sorting can beadapted to work on collections of secret data without leaking anyconfidential information, either directly, indirectly, or through timing behaviour.We pay particular attention to the issue of timing channels caused by cachebehaviour, and argue that it is necessary to disable the effect of the cache in order to construct algorithms manipulating pointers to objectsin such a way that they satisfy the conditions of noninterference.
|
|
| 2. |
- Antignac, Thibaud, 1986, et al.
(författare)
-
Data minimisation: A language-based approach
- 2017
-
Ingår i: IFIP Information Security & Privacy Conference (IFIP SEC'17), volume 502 of IFIP Advances in Information and Communication Technology. pages 442-456. - Cham : Springer Science and Business Media. - 1868-4238 .- 1868-422X. - 9783319584683
-
Konferensbidrag (refereegranskat)abstract
- Data minimisation is a privacy-enhancing principle considered as one of the pillars of personal data regulations. This principle dictates that personal data collected should be no more than necessary for the specific purpose consented by the user. In this paper we study data minimisation from a programming language perspective. We define a data minimiser as a pre-processor for the input which reduces the amount of information available to the program without compromising its functionality. We give its formal definition and provide a procedure to synthesise a correct data minimiser for a given program.
|
|
| 3. |
- Askarov, Aslan, 1981, et al.
(författare)
-
Termination-Insensitive Noninterference Leaks More Than Just a Bit.
- 2008
-
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. - 9783540883128 ; 5283, s. 333-348
-
Konferensbidrag (refereegranskat)abstract
- Current tools for analysing information flow in programs build upon ideas going back to Denning's work from the 70's. These systems enforce an imperfect notion of information flow which has become known as termination-insensitive noninterference. Under this version of noninterference, information leaks are permitted if they are transmitted purely by the program's termination behaviour (i.e., whether it terminates or not). This imperfection is the price to pay for having a security condition which is relatively liberal (e.g. allowing while-loops whose termination may depend on the value of a secret) and easy to check. But what is the price exactly? We argue that, in the presence of output, the price is higher than the ``one bit'' often claimed informally in the literature, and effectively such programs can leak all of their secrets. In this paper we develop a definition of termination-insensitive noninterference suitable for reasoning about programs with outputs. We show that the definition generalises ``batch-job'' style definitions from the literature and that it is indeed satisfied by a Denning-style program analysis with output. Although more than a bit of information can be leaked by programs satisfying this condition, we show that the best an attacker can do is a brute-force attack, which means that the attacker cannot reliably (in a technical sense) learn the secret in polynomial time in the size of the secret. If we further assume that secrets are uniformly distributed, we show that the advantage the attacker gains when guessing the secret after observing a polynomial amount of output is negligible in the size of the secret.
|
|
| 4. |
- Axelsson, Stefan, et al.
(författare)
-
Understanding Intrusion Detection through Visualization
- 2006
-
Bok (övrigt vetenskapligt/konstnärligt)abstract
- Table of contentsForeword by Dr. John McHugh, Canada Research Chair, Director, Privacy and Security Laboratory, Dalhousie University Halifax, N.S. Canada.- Preface.- Introduction.- An Introduction to Intrusion Detection.- The Base-Rate Fallacy and the Difficulty of Intrusion Detection.- Visualising Intrusions: Watching the Webserver.- Combining a Bayesian Classifier with Visualisation.- Visualising the Inner Workings of a Self Learning Classifier.- Visualisation for Intrusion Detection: Hooking the Worm.- References.- Author Index.- Index.
|
|
| 5. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Flow-Sensitive Semantics for Dynamic Information Flow Policies
- 2009
-
Ingår i: ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS 2009). - New York, NY, USA : ACM. - 9781605586458 ; , s. 101-112
-
Konferensbidrag (refereegranskat)abstract
- Dynamic information flow policies, such as declassification, are essential for practically useful information flow control systems. However, most systems proposed to date that handle dynamic information flow policies suffer from a common drawback. They build on semantic models of security which are inherently flow insensitive, which means that many simple intuitively secure programs will be considered insecure. In this paper we address this problem in the context of a particular system, flow locks. We provide a new flow sensitive semantics for flow locks based on a knowledge-style definition (following Askarov and Sabelfeld), in which the knowledge gained by an actor observing a program run is constrained according to the flow locks which are open at the time each observation is made. We demonstrate the applicability of the definition in a soundness proof for a simple flow lock type system. We also show how other systems can be encoded using flow locks, as an easy means to provide these systems with flow sensitive semantics.
|
|
| 6. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Improving the semantics of imperfect security
- 2009
-
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. - 9783642034589 ; 5511 LNCS, s. 88-91
-
Konferensbidrag (refereegranskat)abstract
- Information flow policies that evolve over time (including, for example, declassification) are widely recognised as an essential ingredient in useable information flow control system. In previous work ([BS06a, BS06b]) we have shown one approach to such policies, flow locks, which is a very general and flexible system capable of encoding many other proposed approaches. However, any such policy approach is only useful if we have a precise specification - a semantic model - of what we are trying to enforce. A semantic model gives us insight into what a policy actually guarantees, and defines the precise goals of any enforcement mechanism. Unfortunately, semantic models of declassification can be both inaccurate and difficult to understand. This was definitely the case for the flow locks system as presented in [BS06a, BS06b], and we have found that the main problem is one common to most proposed models to date. We will start by discussing the problem in general, and then go on to sketch its solution for the flow locks system specifically.
|
|
| 7. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Paragon for Practical Programming with Information-Flow Control
- 2013
-
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. - 9783319035413 ; 8301, s. 217-232
-
Konferensbidrag (refereegranskat)abstract
- Conventional security policies for software applications are adequate for managing concerns on the level of access control. But standard abstraction mechanisms of mainstream programming languages are not sufficient to express how information is allowed to flow between resources once access to them has been obtained. In practice we believe that such control - information flow control - is needed to manage the end-to-end security properties of applications.In this paper we present Paragon, a Java-based language with first-class support for static checking of information flow control policies. Paragon policies are specified in a logic-based policy language. By virtue of their explicitly stateful nature, these policies appear to be more expressive and flexible than those used in previous languages with information-flow support.Our contribution is to present the design and implementation of Paragon, which smoothly integrates the policy language with Java’s object-oriented setting, and reaps the benefits of the marriage with a fully fledged programming language.
|
|
| 8. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Paragon - Practical programming with information flow control
- 2017
-
Ingår i: Journal of Computer Security. - 0926-227X. ; 25:4-5, s. 323-365
-
Tidskriftsartikel (refereegranskat)abstract
- Conventional security policies for software applications are adequate for managing concerns on the level of access control. But standard abstraction mechanisms of mainstream programming languages are not sufficient to express how information is allowed to flow between resources once access to them has been obtained. In practice we believe that such control - information flow control - is needed to manage the end-to-end security properties of applications. In this paper we present Paragon, a Java-based language with first-class support for static checking of information flow control policies. Paragon policies are specified in a logic-based policy language. By virtue of their explicitly stateful nature, these policies appear to be more expressive and flexible than those used in previous languages with information-flow support. Our contribution is to present the design and implementation of Paragon, which smoothly integrates the policy language with Java's object-oriented setting, and reaps the benefits of the marriage with a fully fledged programming language.
|
|
| 9. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Paragon: Programming with information flow control (demo)
- 2014
-
Ingår i: 9th Workshop on Programming Languages and Analysis for Security, PLAS 2014; Uppsala; Sweden; 28 July 2014 through 1 August 2014. - New York, NY, USA : ACM. - 9781450328623 ; , s. 79-80
-
Konferensbidrag (refereegranskat)abstract
- We demonstrate Paragon, a Java-based programming language with integrated information-flow control. We show how the use of information-flow policies combined with encapsulation allows for simple yet powerful and flexible policy libraries tailored to the needs of a particular application or system.
|
|
| 10. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Paralocks: Role-based information flow control and beyond
- 2010
-
Ingår i: 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10, Madrid, Spain, 17-23 January 2010. - New York, NY, USA : ACM. - 0730-8566. - 9781605584799 ; , s. 431-444
-
Konferensbidrag (refereegranskat)abstract
- This paper presents Paralocks, a language for building expressive but statically verifiable fine-grained information flow policies. Paralocks combine the expressive power of Flow Locks (Broberg & Sands, ESOP'06) with the ability to express policies involving run-time principles, roles (in the style of role-based access control), and relations (such as "acts-for" in discretionary access control). We illustrate the Paralocks policy language by giving a simple encoding of Myers and Liskov's Decentralized Label Model (DLM). Furthermore - and unlike the DLM - we provide an information flow semantics for full Paralock policies. Lastly we illustrate how Paralocks can be statically verified by providing a simple programming language incorporating Paralock policy specifications, and a static type system which soundly enforces information flow security according to the Paralock semantics.
|
|
| 11. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Paralocks - Role-Based Information Flow Control and Beyond
- 2010
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - : Association for Computing Machinery (ACM). - 0730-8566 .- 0362-1340 .- 1558-1160. ; 45:1, s. 431-444
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents Paralocks, a language for building expressive but statically verifiable fine-grained information flow policies. Paralocks combine the expressive power of Flow Locks (Broberg & Sands, ESOP'06) with the ability to express policies involving runtime principles, roles (in the style of role-based access control), and relations (such as "acts-for" in discretionary access control). We illustrate the Paralocks policy language by giving a simple encoding of Myers and Liskov's Decentralized Label Model (DLM). Furthermore - and unlike the DLM - we provide an information flow semantics for full Paralock policies. Lastly we illustrate how Paralocks can be statically verified by providing a simple programming language incorporating Paralock policy specifications, and a static type system which soundly enforces information flow security according to the Paralock semantics.
|
|
| 12. |
- Broberg, Niklas, 1979, et al.
(författare)
-
The Anatomy and Facets of Dynamic Policies
- 2015
-
Ingår i: Proceedings. The Computer Security Foundations Workshop III. - 1063-6900. - 9781467375382 ; 2015-September, s. 122-136
-
Konferensbidrag (refereegranskat)abstract
- Information flow policies are often dynamic; the security concerns of a program will typically change during execution to reflect security-relevant events. A key challenge is how to best specify, and give proper meaning to, such dynamic policies. A large number of approaches exist that tackle that challenge, each yielding some important, but unconnected, insight. In this work we synthesise existing knowledge on dynamic policies, with an aim to establish a common terminology, best practices, and frameworks for reasoning about them. We introduce the concept of facets to illuminate subtleties in the semantics of policies, and closely examine the anatomy of policies and the expressiveness of policyspecification mechanisms. We further explore the relation between dynamic policies and the concept of declassification.
|
|
| 13. |
- Broberg, Niklas, 1979, et al.
(författare)
-
Towards a core calculus for dynamic flow policies
- 2006
-
Ingår i: Programming Languages and Systems. 15th European Symposium on Programming, ESOP 2006. - Berlin, Heidelberg : Springer Berlin Heidelberg. ; 3924, s. 180-196
-
Konferensbidrag (refereegranskat)abstract
- Security is rarely a static notion. What is considered to be confidential or untrusted data varies over time according to changing events and states. The static verification of secure information flow has been a popular theme in recent programming language research, but information flow policies considered are based on multilevel security which presents a static view of security levels. In this paper we introduce a very simple mechanism for specifying dynamic information flow policies, flow locks, which specify conditions under which data may be read by a certain actor. The interface between the policy and the code is via instructions which open and close flow locks. We present a type and effect system for an ML-like language with references which permits the completely static verification of flow lock policies, and prove that the system satisfies a semantic security property generalising noninterference. We show that this simple mechanism can represent a number of recently proposed information flow paradigms for declassification.
|
|
| 14. |
|
|
| 15. |
- Del Tedesco, Filippo, 1983, et al.
(författare)
-
A Semantic Hierarchy for Erasure Policies
- 2011
-
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. - 9783642255595 ; 7093, s. 352-369
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of logical data erasure, contrasting with physical erasure in the same way that end-to-end information flow control contrasts with access control. We present a semantic hierarchy for erasure policies, using a possibilistic knowledge-based semantics to define policy satisfaction such that there is an intuitively clear upper bound on what information an erasure policy permits to be retained. Our hierarchy allows a rich class of erasure policies to be expressed, taking account of the power of the attacker, how much information may be retained, and under what conditions it may be retained. While our main aim is to specify erasure policies, the semantic framework allows quite general information-flow policies to be formulated for a variety of semantic notions of secrecy.
|
|
| 16. |
- Del Tedesco, Filippo, 1983, et al.
(författare)
-
A user model for information erasure.
- 2009
-
Ingår i: Proceedings 7th International Workshop on Security Issues in Concurrency, Bologna (Italy), 5th September 2009. ; EPTCS 7
-
Konferensbidrag (refereegranskat)abstract
- Hunt and Sands (ESOP'08) studied a notion of information erasure for systems which receive secrets intended for limited-time use. Erasure demands that once a secret has fulfilled its purpose the subsequent behaviour of the system should reveal no information about the erased data. In this paper we address a shortcoming in that work: for erasure to be possible the user who provides data must also play his part, but previously that role was only specified informally. Here we provide a formal model of the user and a collection of requirements called erasure friendliness. We prove that an erasure-friendly user can be composed with an erasing system (in the sense of Hunt and Sands) to obtain a combined system which is jointly erasing in an appropriate sense. In doing so we identify stronger requirements on the user than those informally described in the previous work.
|
|
| 17. |
- Del Tedesco, Filippo, 1983, et al.
(författare)
-
Fault-resilient non-interference
- 2016
-
Ingår i: Proceedings - IEEE Computer Security Foundations Symposium. - 1940-1434. - 9781509026074 ; 2016-August, s. 401-416
-
Konferensbidrag (refereegranskat)abstract
- Environmental noise (e.g. heat, ionized particles, etc.) causes transient faults in hardware, which lead to corruption of stored values. Mission-critical devices require such faults to be mitigated by fault-tolerance - a combination of techniques that aim at preserving the functional behaviour of a system despite the disruptive effects of transient faults. Fault-tolerance typically has a high deployment cost - special hardware might be required to implement it - and provides weak statistical guarantees. It is also based on the assumption that faults are rare. In this paper, we consider scenarios where security, rather than functional correctness, is the main asset to be protected. Our main contribution is a theory for expressing confidentiality of data in the presence of transient faults. We show that the natural probabilistic definition of security in the presence of faults can be captured by a possibilistic definition. Furthermore, the possibilistic definition is implied by a known bisimulation-based property, called Strong Security. We illustrate the utility of these results for a simple RISC architecture for which only the code memory and program counter are assumed fault-tolerant. We present a type-directed compilation scheme that produces RISC code from a higher-level language for which Strong Security holds - i.e. well-typed programs compile to RISC code which is secure despite transient faults. In contrast with fault-tolerance solutions, our technique assumes relatively little special hardware, gives formal guarantees, and works in the presence of an active attacker who aggressively targets parts of a system and induces faults precisely.
|
|
| 18. |
- Del Tedesco, Filippo, 1983, et al.
(författare)
-
Fault-tolerant Non-interference
- 2014
-
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. - 9783319048963 ; 8364 LNCS, s. 60-76
-
Konferensbidrag (refereegranskat)abstract
- This paper is about ensuring security in unreliable systems. We studysystems which are subject to transient faults – soft errors that cause stored valuesto be corrupted. The classic problem of fault tolerance is to modify a system sothat it works despite a limited number of faults. We introduce a novel variantof this problem. Instead of demanding that the system works despite faults, wesimply require that it remains secure: wrong answers may be given but secretswill not be revealed. We develop a software-based technique to achieve this fault tolerantnon-interference property. The method is defined on a simple assemblylanguage, and guarantees security for any assembly program provided as input.The security property is defined on top of a formal model that encompasses boththe fault-prone machine and the faulty environment. A precise characterization ofthe class of programs for which the method guarantees transparency is provided.
|
|
| 19. |
- Del Tedesco, Filippo, 1983, et al.
(författare)
-
Implementing Erasure Policies Using Taint Analysis
- 2012
-
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. ; 7127, s. 193-209
-
Konferensbidrag (refereegranskat)abstract
- Security or privacy-critical applications often require access to sensitive information in order to function. But in accordance with the principle of least privilege – or perhaps simply for legal compliance – such applications should not retain said information once it has served its purpose. In such scenarios, the timely disposal of data is known as an information erasure policy. This paper studies software-level information erasure policies for the data manipulated by programs. The paper presents a new approach to the enforcement of such policies. We adapt ideas from dynamic taint analysis to track how sensitive data sources propagate through a program and erase them on demand. The method is implemented for Python as a library, with no modifications to the runtime system. The library is easy to use, and allows programmers to indicate information-erasure policies with only minor modifications to their code.
|
|
| 20. |
- Demange, D., et al.
(författare)
-
All Secrets Great and Small
- 2009
-
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. - 9783642005893 ; 5502, s. 207-221
-
Konferensbidrag (refereegranskat)abstract
- Tools for analysing secure information flow are almost exclusively based on ideas going back to Denning's work from the 70's. This approach embodies an imperfect notion of security which turns a blind eye to information flows which are encoded in the termination behaviour of a program. In exchange for this weakness many more programs are deemed "secure", using conditions which are easy to check. Previously it was thought that such leaks are limited to at most one bit per run. Recent work by Askarov et al (ESORICS'08) offers some bad news and some good news: the bad news is that for programs which perform output, the amount of information leaked by a Denning style analysis is not bounded; the good news is that if secrets are chosen to be sufficiently large and sufficiently random then they cannot be effectively leaked at all. The problem addressed in this paper is that secrets cannot always be made sufficiently large or sufficiently random. Contrast, for example, an encryption key with an "hasHIV"-field of a patient record. In recognition of this we develop a notion of secret-sensitive noninterference in which "small" secrets are handled more carefully than "big" ones. We illustrate the idea with a type system which combines a liberal Denning-style analysis with a more restrictive system according to the nature of the secrets at hand.
|
|
| 21. |
- Ebadi Tavallaei, Hamid, 1987, et al.
(författare)
-
Differential Privacy: Now it’s Getting Personal
- 2015
-
Ingår i: ACM SIGPLAN Notices. - New York, NY, USA : ACM. - 1523-2867 .- 0362-1340 .- 1558-1160. ; 50:1, s. 69-81
-
Tidskriftsartikel (refereegranskat)abstract
- Differential privacy provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge. Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction. This paper is about a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy (PDP). In PDP each individual has its own personal privacy level. We describe ProPer, a interactive system for implementing PDP which maintains a privacy budget for each individual. When a primitive query is made on data derived from individuals, the provenance of the involved records determines how the privacy budget of an individual is affected: the number of records derived from Alice determines the multiplier for the privacy decrease in Alice's budget. This offers some advantages over previous systems, in particular its fine-grained character allows better utilisation of the privacy budget than mechanisms based purely on the concept of global sensitivity, and it applies naturally to the case of a live database where new individuals are added over time. We provide a formal model of the ProPer approach, prove that it provides personalised differential privacy, and describe a prototype implementation based on McSherry's PINQ system.
|
|
| 22. |
- Ebadi Tavallaei, Hamid, 1987, et al.
(författare)
-
Featherweight PINQ
- 2016
-
Ingår i: Journal of Privacy and Confidentiality. - 2575-8527. ; 7:2, s. 159-164
-
Tidskriftsartikel (refereegranskat)abstract
- Differentially private mechanisms enjoy a variety of composition properties. Leveraging these, McSherry introduced PINQ (SIGMOD 2009), a system empowering non-experts to construct new differentially private analyses. PINQ is an LINQ-like API which provides automatic privacy guarantees for all programs which use it to mediate sensitive data manipulation. In this work we introduce featherweight PINQ , a formal model capturing the essence of PINQ. We prove that any program interacting with featherweight PINQ’s API is differentially private.
|
|
| 23. |
- Ebadi Tavallaei, Hamid, 1987, et al.
(författare)
-
Sampling and Partitioning for Differential Privacy
- 2016
-
Ingår i: Privacy Security & Trust Conference 2016. - 9781509043798 ; , s. 664-673
-
Konferensbidrag (refereegranskat)abstract
- Differential privacy enjoys increasing popularity thanks to both a precise semantics for privacy and effective enforcement mechanisms. Many tools have been proposed to spread its use and ease the task of the concerned data scientist. The most promising among them completely discharge the user of the privacy concerns by transparently taking care of the privacy budget. However, their implementation proves to be delicate, and introduce flaws by falsifying some of the theoretical assumptions made to guarantee differential privacy. Moreover, such tools rely on assumptions leading to over-approximations which artificially reduce utility. In this paper we focus on a key mechanism that tools do not support well: sampling. We demonstrate an attack on PINQ (McSherry, SIGMOD 2009), one of these tools, relying on the difference between its internal mechanics and the formal theory for the sampling operation, and study a range of sampling methods and show how they can be correctly implemented in a system for differential privacy.
|
|
| 24. |
- Gissurarson, Matthías Páll, 1991, et al.
(författare)
-
PropR: Property-Based Automatic Program Repair
- 2022
-
Ingår i: Proceedings - International Conference on Software Engineering. - New York, NY, USA : ACM. - 0270-5257. ; 2022-May
-
Konferensbidrag (refereegranskat)abstract
- Automatic program repair (APR) regularly faces the challenge of overfitting patches - patches that pass the test suite, but do not actually address the problems when evaluated manually. Currently, overfit detection requires manual inspection or an oracle making quality control of APR an expensive task. With this work, we want to introduce properties in addition to unit tests for APR to address the problem of overfitting. To that end, we design and implement PropR, a program repair tool for Haskell that leverages both property-based testing (via QuickCheck) and the rich type system and synthesis offered by the Haskell compiler. We compare the repair-ratio, time-to-first-patch and overfitting-ratio when using unit tests, property-based tests, and their combination. Our results show that properties lead to quicker results and have a lower overfit ratio than unit tests. Our results show that while the total number of fixes is reduced, the ratio of overfit patches greatly declines. The created overfit patches provide valuable insight into the underlying problems of the program to repair (e.g., in terms of fault localization or test quality). We consider this step towards fitter, or at least insightful, patches a critical contribution to bring APR into developer workflows.
|
|
| 25. |
- Gustavsson, Jörgen, et al.
(författare)
-
Possibilities and Limitations of Call-by-Need Space Improvement
- 2001
-
Ingår i: Proceeding of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP'01). ; , s. 265-276
-
Konferensbidrag (refereegranskat)abstract
- Innocent-looking program transformations can easily change the space complexity of lazy functional programs. The theory of space improvement seeks to characterise those local program transformations which are guaranteed never to worsen asymptotic space complexity of any program. Previous work by the authors introduced the space improvement relation and showed that a number of simple local transformation laws are indeed space improvements. This paper seeks an answer to the following questions: is the improvement relation inhabited by interesting program transformations, and, if so, how might they be established? We show that the asymptotic space improvement relation is semantically badly behaved, but that the theory of strong space improvement possesses a fixed-point induction theorem which permits the derivation of improvement properties for recursive definitions. With the help of this tool we explore the landscape of space improvement byconsidering a range of classical program transformations.
|
|
| 26. |
- Hedin, Daniel, 1978, et al.
(författare)
-
Noninterference in the presence of non-opaque pointers
- 2006
-
Ingår i: Proceedings of the 19th IEEE Computer Security Foundations Workshop. ; , s. 255-269
-
Konferensbidrag (refereegranskat)abstract
- A common theoretical assumption in the study of information flow security in Java-like languages is that pointers are opaque - i.e., that the only properties that can be observed of pointers are the objects to which they point, and (at most) their equality. These assumptions often fail in practice. For example, various important operations in Java's standard API, such as hashcodes or serialization, might break pointer opacity. As a result, information-flow static analyses which assume pointer opacity risk being unsound in practice, since the pointer representation provides an unchecked implicit leak. We investigate information flow in the presence of non-opaque pointers for an imperative language with records, pointer instructions and exceptions, and develop an information flow aware type system which guarantees noninterference.
|
|
| 27. |
- Hedin, Daniel, 1978, et al.
(författare)
-
Timing Aware Information Flow Security for a JavaCard-like Bytecode
- 2005
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 141:1, s. 163-182
-
Konferensbidrag (refereegranskat)abstract
- Common protection mechanisms fail to provide end-to-end security; programs with legitimate access to secret information are not prevented from leaking this to the world. Information-flow aware analyses track the flow of information through the program to prevent such leakages, but often ignore information flows through covert channels even though they pose a serious threat. A typical covert channel is to use the timing of certain events to carry information. We present a timing-aware information-flow type system for a low-level language similar to a non-trivial subset of a sequential Java bytecode. The type system is parameterized over the time model of the instructions of the language and over the algorithm enforcing low-observational equivalence, used in the prevention of implicit and timing flows.
|
|
| 28. |
- Hunt, Leo Sebastian, 1960, et al.
(författare)
-
A Quantale of Information
- 2021
-
Ingår i: Proceedings - IEEE Computer Security Foundations Symposium. - 1940-1434. - 9781728176079 ; 2021-June, s. 94-108
-
Konferensbidrag (refereegranskat)abstract
- Information flow properties are the semantic cornerstone of a wide range of program transformations, program analyses, and security properties. The variety of information that can be transmitted from inputs to outputs in a deterministic system can be captured by representing information as equivalence relations over the sets of possible values, using an equivalence relation on the input domain to model what may be learned, and an equivalence relation on the output to model what may be observed. The set of equivalence relations over a given set of values form a lattice, where the partial order models containment of information, and lattice join models the effect of combining information. This elegant and general structure is sometimes referred to as the lattice of information.In this paper we identify an abstraction of information flow which has not been studied previously, namely disjunctive dependency (depending on x or y, as distinct from depending on both x and y). We argue that this refines the space of semantic models for dependency in a way which is both interesting in its own right and which has applications in security settings of practical interest (in particular, where so-called “Chinese wall policies” are in effect).To model disjunctive dependency we introduce a nontrivial generalisation of the lattice of information in the form of a richer structure, built on sets of equivalence relations closed under a novel condition called tiling-closure. This structure forms a quantale - a lattice equipped with a tensor operation - in which lattice join corresponds to disjunctive combination of information, and tensor corresponds to conjunctive combination. Using this we generalise the definition of information flow properties, and show that the definition has the key properties needed to support compositional reasoning about programs.
|
|
| 29. |
- Hunt, Sebastian, et al.
(författare)
-
From Exponential to Polynomial-time Security Typing via Principal Types
- 2011
-
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. - 9783642197178 ; 6602, s. 297-316
-
Konferensbidrag (refereegranskat)abstract
- Hunt and Sands (POPL'06) studied a flow sensitive type (FST) system for multi-level security, parametric in the choice of lattice of security levels. Choosing the powerset of program variables as the security lattice yields a system which was shown to be equivalent to Amtoft and Banerjee's Hoare-style independence logic (SAS'04). Moreover, using the powerset lattice, it was shown how to derive a principal type from which all other types (for all choices of lattice) can be simply derived. Both of these earlier works gave "algorithmic" formulations of the type system/program logic, but both algorithms are of exponential complexity due to the iterative typing of While loops. Later work by Hunt and Sands (ESOP'08) adapted the FST system to provide an erasure type system which determines whether some input is correctly erased at a designated time. This type system is inherently exponential, requiring a double typing of the erasure-labelled input command. In this paper we start by developing the FST work in two key ways: (1) We specialise the FST system to a form which only derives principal types; the resulting type system has a simple algorithmic reading, yielding principal security types in polynomial time. (2) We show how the FST system can be simply extended to check for various degrees of termination sensitivity (the original FST system is completely termination insensitive, while the erasure type system is fully termination sensitive).We go on to demonstrate the power of these techniques by combining them to develop a type system which is shown to correctly implement erasure typing in polynomial time. Principality is used in an essential way to reduce type derivation size from exponential to linear.
|
|
| 30. |
|
|
| 31. |
- Hunt, Sebastian, et al.
(författare)
-
New Program Abstractions for Privacy
- 2020
-
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. ; 12065 LNCS, s. 256-267
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- Static program analysis, once seen primarily as a tool for optimising programs, is now increasingly important as a means to provide quality guarantees about programs. One measure of quality is the extent to which programs respect the privacy of user data. Differential privacy is a rigorous quantified definition of privacy which guarantees a bound on the loss of privacy due to the release of statistical queries. Among the benefits enjoyed by the definition of differential privacy are compositionality properties that allow differentially private analyses to be built from pieces and combined in various ways. This has led to the development of frameworks for the construction of differentially private program analyses which are private-by-construction. Past frameworks assume that the sensitive data is collected centrally, and processed by a trusted curator. However, the main examples of differential privacy applied in practice - for example in the use of differential privacy in Google Chrome’s collection of browsing statistics, or Apple’s training of predictive messaging in iOS 10 -use a purely local mechanism applied at the data source, thus avoiding the collection of sensitive data altogether. While this is a benefit of the local approach, with systems like Apple’s, users are required to completely trust that the analysis running on their system has the claimed privacy properties. In this position paper we outline some key challenges in developing static analyses for analysing differential privacy, and propose novel abstractions for describing the behaviour of probabilistic programs not previously used in static analyses.
|
|
| 32. |
- Hunt, Sebastian, et al.
(författare)
-
On flow-sensitive security types
- 2006
-
Ingår i: POPL'06, Proceedings of the 33rd Annual. ACM SIGPLAN - SIGACT. Symposium on Principles of Programming Languages.
-
Konferensbidrag (refereegranskat)abstract
- This article investigates formal properties of a family of semantically sound flow-sensitive type systems for tracking information flow in simple While programs. The family is indexed by the choice of flow lattice. By choosing the flow lattice to be the powerset of program variables, we obtain a system which, in a very strong sense, subsumes all other systems in the family (in particular, for each program, it provides a principal typing from which all others may be inferred). This distinguished system is shown to be equivalent to, though more simply described than, Amtoft and Banerjee's Hoare-style independence logic (SAS'04). In general, some lattices are more expressive than others. Despite this, we show that no type system in the family can give better results for a given choice of lattice than the type system for that lattice itself. Finally, for any program typeable in one of these systems, we show how to construct an equivalent program which is typeable in a simple flow-insensitive system. We argue that this general approach could be useful in a proof-carrying-code setting.
|
|
| 33. |
- Hunt, Sebastian, et al.
(författare)
-
Reconciling Shannon and Scott with a Lattice of Computable Information
- 2023
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 7, s. 1987-2016
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon (some five years after the publication of his celebrated quantitative theory of communication), describes how the information content of channels can be described qualitatively, but still abstractly, in terms of information elements, where information elements can be viewed as equivalence relations over the data source domain. Shannon showed that these elements have a partial ordering, expressing when one information element is more informative than another, and that these partially ordered information elements form a complete lattice. In the context of security and information flow this structure has been independently rediscovered several times, and used as a foundation for understanding and reasoning about information flow. The second theory of information is Dana Scott's domain theory, a mathematical framework for giving meaning to programs as continuous functions over a particular topology. Scott's partial ordering also represents when one element is more informative than another, but in the sense of computational progress - i.e. when one element is a more defined or evolved version of another. To give a satisfactory account of information flow in computer programs it is necessary to consider both theories together, in order to understand not only what information is conveyed by a program (viewed as a channel, à la Shannon) but also how the precision with which that information can be observed is determined by the definedness of its encoding (à la Scott). To this end we show how these theories can be fruitfully combined, by defining the Lattice of Computable Information (LoCI), a lattice of preorders rather than equivalence relations. LoCI retains the rich lattice structure of Shannon's theory, filters out elements that do not make computational sense, and refines the remaining information elements to reflect how Scott's ordering captures possible varieties in the way that information is presented. We show how the new theory facilitates the first general definition of termination-insensitive information flow properties, a weakened form of information flow property commonly targeted by static program analyses.
|
|
| 34. |
- Magazinius, Jonas, 1981, et al.
(författare)
-
Safe Wrappers and Sane Policies for Self Protecting JavaScript
- 2012
-
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. ; 7127, s. 239-255
-
Konferensbidrag (refereegranskat)abstract
- Phung et al (ASIACCS’09) describe a method for wrapping built-in functions of JavaScript programs in order to enforce security policies. The method is appealing because it requires neither deep transformation of the code norbrowser modification. Unfortunately the implementation outlined suffers from a range of vulnerabilities, and policy construction is restrictive and error prone. In this paper we address these issues to provide a systematic way to avoid the identified vulnerabilities, and make it easier for the policy writer to construct declarative policies – i.e. policies upon which attacker code has no side effects.
|
|
| 35. |
- Mantel, A., et al.
(författare)
-
Assumptions and guarantees for compositional noninterference
- 2011
-
Ingår i: Proceedings - IEEE Computer Security Foundations Symposium. - 1940-1434. - 9780769543659 ; , s. 218-232
-
Konferensbidrag (refereegranskat)abstract
- The idea of building secure systems by plugging together "secure" components is appealing, but this requires a definition of security which, in addition to taking care of top-level security goals, is strengthened appropriately in order to be compositional. This approach has been previously studied for information-flow security of shared-variable concurrent programs, but the price for compositionality is very high: a thread must be extremely pessimistic about what an environment might do with shared resources. This pessimism leads to many intuitively secure threads being labelled as insecure. Since in practice it is only meaningful to compose threads which follow an agreed protocol for data access, we take advantage of this to develop a more liberal compositional security condition. The idea is to give the security definition access to the intended pattern of data usage, as expressed by assumption-guarantee style conditions associated with each thread. We illustrate the improved precision by developing the first flow-sensitive security type system that provably enforces a noninterference-like property for concurrent programs. © 2011 IEEE.
|
|
| 36. |
- Mantel, Heiko, et al.
(författare)
-
Controlled Declassification based on Intransitive Noninterference
- 2004
-
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. - 9783540237242 ; 3302, s. 129-145
-
Konferensbidrag (refereegranskat)abstract
- Traditional noninterference cannot cope with common features of secure systems like channel control, information filtering, or explicit downgrading. Recent research has addressed the derivation and use of weaker security conditions that could support such features in a language-based setting. However, a fully satisfactory solution to the problem has yet to be found. A key problem is to permit exceptions to a given security policy without permitting too much. In this article, we propose an approach that draws its underlying ideas from intransitive noninterference, a concept usually used on a more abstract specification level. Our results include a new bisimulation-based security condition that controls tightly where downgrading can occur and a sound security type system for checking this condition.
|
|
| 37. |
|
|
| 38. |
- Moran, Andrew, et al.
(författare)
-
Erratic fudgets: a semantic theory for an embedded coordination language
- 2003
-
Ingår i: Science of Computer Programming. - 0167-6423. ; 46:1-2, s. 99-135
-
Tidskriftsartikel (refereegranskat)abstract
- The powerful abstraction mechanisms of functional programming languagesprovide the means to develop domain-specific programming languages within thelanguage itself. Typically, this is realised by designing a set ofcombinators (higher-order reusable programs) for an application area, and byconstructing individual applications by combining and coordinating individualcombinators. This paper is concerned with a successful example of such anembedded programming language, namely Fudgets, a library of combinators forbuilding graphical user interfaces in the lazy functional language Haskell.The Fudget library has been used to build a number of substantialapplications, including a web browser and a proof editor interface to a proofchecker for constructive type theory. This paper develops a semantic theoryfor the non-deterministic stream processors that are at the heart of theFudget concept. The interaction of two features of stream processors makes thedevelopment of such a semantic theory problematic:(i) the sharing of computation provided by the lazy evaluation mechanism of the underlying host language, and(ii) the addition of non-deterministic choice needed to handle the natural concurrency that reactive applications entail.We demonstrate that this combination of features in a higher-order functionallanguage can be tamed to provide a tractable semantics theory and inductionprinciples suitable for reasoning about contextual equivalence of Fudgets.
|
|
| 39. |
- Nielson, Flemming, et al.
(författare)
-
Preface
- 2019
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 11426 LNCS
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)
|
|
| 40. |
- Phung, Phu, 1979, et al.
(författare)
-
Lightweight Self-Protecting JavaScript
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper introduces a method to control JavaScript execution. The aimis to prevent or modify inappropriate behaviour caused by e.g. maliciousinjected scripts or poorly designed third-party code. The approach is basedon modifying the code so as to make it self-protecting: the protection mecha-nism (security policy) is embedded into the code itself and intercepts securityrelevant API calls. The challenges come from the nature of the JavaScriptlanguage: any variables in the scope of the program can be redefined, andcode can be created and run on-the-fly. This creates potential problems,respectively, for tamper-proofing the protection mechanism, and for ensur-ing that no security relevant events bypass the protection. Unlike previousapproaches to instrument and monitor JavaScript to enforce or adjust be-haviour, the solution we propose is lightweight in that (i) it does not requirea modified browser, and (ii) it does not require any run-time parsing andtransformation of code (including dynamically generated code). As a result,the method has low run-time overhead compared to other methods satisfying(i), and the lack of need for browser modifications means that the policy caneven be applied on the server to mitigate some effects of cross-site scriptingbugs. We describe the implementation, and present an abstract formalisationof the basic method. Based on this formalisation we show, as an example,that it can soundly enforce the class of policies known as security automata.
|
|
| 41. |
- Phung, Phu, 1979, et al.
(författare)
-
Lightweight Self-Protecting JavaScript
- 2009
-
Ingår i: Proceedings of ACM Symposium on Information, Computer and Communications Security (ASIACCS 2009). - New York, NY, USA : ACM. - 9781605583945 ; , s. 47-60
-
Konferensbidrag (refereegranskat)abstract
- This paper introduces a method to control JavaScript execution. The aim is to prevent or modify inappropriate behaviour caused by e.g. malicious injected scripts or poorly designed third-party code. The approach is based on modifying the code so as to make it self-protecting: the protection mechanism (security policy) is embedded into the code itself and intercepts security relevant API calls. The challenges come from the nature of the JavaScript language: any variables in the scope of the program can be redefined, and code can be created and run on-the-fly. This creates potential problems, respectively, for tamper-proofing the protection mechanism, and for ensuring that no security relevant events bypass the protection. Unlike previous approaches to instrument and monitor JavaScript to enforce or adjust behaviour, the solution we propose is lightweight in that (i) it does not require a modified browser, and (ii) it does not require any run-time parsing and transformation of code (including dynamically generated code). As a result, the method has low run-time overhead compared to other methods satisfying (i), and the lack of need for browser modifications means that the policy can even be applied on the server to mitigate some effects of cross-site scripting bugs.
|
|
| 42. |
- Phung, Phu, 1979, et al.
(författare)
-
Security Policy Enforcement for the OSGi Framework Using Aspect-Oriented Programming
- 2008
-
Ingår i: Proceedings of the 32nd Annual International Computer Software and Applications Conference (COMPSAC 2008), 28 July - 01 August 2008, Turku, Finland. IEEE Computer Society 2008. - 0730-3157. ; , s. 1076-1082
-
Konferensbidrag (refereegranskat)abstract
- The lifecycle mismatch between vehicles and their IT system poses a problem for the automotive industry. Such systems need to be open and extensible to provide customised functionalities and services. What is less clear is how to achieve this with quality and security guarantees. Recent studies in language-based security -- the use of programming language technology to enforce application specific security policies -- show that security policy enforcement mechanisms such as inlined reference monitors provide a potential solution for security in extensible systems. In this paper we study the implementation of security policyenforcement using aspect-oriented programming for the OSGi(Open Services Gateway initiative) framework.We identify classes of reference monitor-style policies that can be defined and enforced using AspectJ, a well-known aspect-oriented programming language. We demonstrate the use of security states to describe history-based policies. We also introduce and implement various levels of security states in Java to describe session level history versus global application level history. We illustrate the effectiveness of the implementation by deploying the security policy enforcement solution in an examplescenario of software downloading in a standard vehicle system.
|
|
| 43. |
- Pinisetty, Srinivas, et al.
(författare)
-
Runtime verification of hyperproperties for deterministic programs
- 2018
-
Ingår i: Proceedings - International Conference on Software Engineering. - New York, NY, USA : ACM. - 0270-5257. - 9781450357180 ; , s. 20-29
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we consider the runtime verification problem of safety hyperproperties for deterministic programs. Several security and information-flow policies such as data minimality, non-interference, integrity, and software doping are naturally expressed formally as safety hyperproperties. Although there are monitoring results for hyperproperties, the algorithms are very complex since these are properties over set of traces, and not over single traces. For the deterministic input-output programs that we consider, and the specific safety hyperproperties we are interested in, the problem can be reduced to monitoring of trace properties. In this paper, we present a simpler monitoring approach for safety hyperproperties of deterministic programs. The approach involves transforming the given safety hyperproperty into a trace property, extracting a characteristic predicate for the given hyperproperty, and providing a parametric monitor taking such predicate as parameter. For any hyperproperty in the considered subclass, we show how runtime verification monitors can be synthesised. We have implemented our approach in the form of a parameterised monitor for the given class, and have applied it to a number of hyperproperties including data minimisation, non-interference, integrity and software doping. We show results concerning both offline and online monitoring.
|
|
| 44. |
- Sabelfeld, Andrei, 1974, et al.
(författare)
-
A Per Model of Secure Information Flow in Sequential Programs
- 2001
-
Ingår i: Higher-Order and Symbolic Computation. ; 14:1, s. 59-91
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature, and connections to other forms of program analysis. The approach is inspired by (and equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and partially confidential data. We extend the approach to handle nondeterminism by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics.
|
|
| 45. |
- Sabelfeld, Andrei, 1974, et al.
(författare)
-
Declassification: Dimensions and Principles
- 2009
-
Ingår i: Journal of Computer Security. - 0926-227X. ; 17:5, s. 517-548
-
Tidskriftsartikel (refereegranskat)abstract
- Computing systems often deliberately release (or declassify) sensitive information. A principal security concern for systems permitting information release is whether this release is safe: is it possible that the attacker compromises the information release mechanism and extracts more secret information than intended? While the security community has recognised the importance of the problem, the state-of-the-art in information release is, unfortunately, a number of approaches with somewhat unconnected semantic goals. We provide a road map of the main directions of current research, by classifying the basic goals according to what information is released, who releases information, where in the system information is released and when information can be released. With a general declassification framework as a long-term goal, we identify some prudent principles of declassification. These principles shed light on existing definitions and may also serve as useful “sanity checks" for emerging models.
|
|
| 46. |
|
|
| 47. |
- Sabelfeld, Andrei, 1974, et al.
(författare)
-
Probabilistic Noninterference for Multi-threaded Programs
- 2000
-
Ingår i: Proceedings of the 13th IEEE Computer Security Foundations Workshop. ; , s. 200-214
-
Konferensbidrag (refereegranskat)abstract
- A program which has access to your sensitive data presents a security threat. Does the program keep your secrets secret? To answer the question one must specify what it means for a program to be secure, and one may wish to verify the security specification before executing the program. We present a probability-sensitive security specification (probabilistic noninterference) for multi-threaded programs based on a probabilistic bisimulation. Some previous approaches to specifying confidentiality rely on a particular scheduler for executing program threads. This is unfortunate since scheduling policy is typically outside the language specification for multi-threaded languages. We describe how to generalise noninterference in order to define robust security with respect to any particular scheduler used and show, for a simple imperative language with dynamic thread creation, how the security condition satisfies compositionality properties which facilitates a straightforward proof of correctness of e.g. security type systems.
|
|
| 48. |
- Sands, David, 1965, et al.
(författare)
-
Lambda Calculi and Linear Speedups
- 2002
-
Ingår i: The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540003267
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- The equational theories at the core of most functional programming are variations on the standard lambda calculus. The best known of these is the call-by-value lambda calculus whose core is the value-beta computation rule (λχ.M) V → M[V/χ] where V is restricted to be a value rather than an arbitrary term. This paper investigates the transformational power of this core theory of functional programming. The main result is that the equational theory of the call-by-value lambda calculus cannot speed up (or slow down) programs by more than a constant factor. The corresponding result also holds for call-by-need but we show that it does not hold for call-byname: there are programs for which a single beta reduction can change the program’s asymptotic complexity.
|
|
| 49. |
- Svenningsson, Josef, 1976, et al.
(författare)
-
Specification and Verification of Side Channel Declassification
- 2009
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Side channel attacks have emerged as a serious threat to the security of both networked and embedded systems -- in particular through the implementations of cryptographic operations. Side channels can be difficult to model formally, but with careful coding and program transformation techniques it may be possible to verify security in the presence of specific side-channel attacks. But what if a program intentionally makes a tradeoff between security and efficiency and leaks some information through a side channel? In this paper we study such tradeoffs using ideas from recent research on declassification. We present a semantic model of security for programs which allow for declassification through side channels, and show how side-channel declassification can be verified using off-the-shelf software model checking tools. Finally, to make it simpler for verifiers to check that a program conforms to a particular side-channel declassification policy we introduce a further tradeoff between efficiency and verifiability: by writing programs in a particular ``manifest form'' security becomes considerably easier to verify.
|
|
| 50. |
- Svenningsson, Josef, 1976, et al.
(författare)
-
Specification and Verification of Side Channel Declassification
- 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. - 9783642124587 ; 5983, s. 111-125
-
Konferensbidrag (refereegranskat)abstract
- Side channel attacks have emerged as a serious threat to the security of both networked and embedded systems -- in particular through the implementations of cryptographic operations. Side channels can be difficult to model formally, but with careful coding and program transformation techniques it may be possible to verify security in the presence of specific side-channel attacks. But what if a program intentionally makes a tradeoff between security and efficiency and leaks some information through a side channel? In this paper we study such tradeoffs using ideas from recent research on declassification. We present a semantic model of security for programs which allow for declassification through side channels, and show how side-channel declassification can be verified using off-the-shelf software model checking tools. Finally, to make it simpler for verifiers to check that a program conforms to a particular side-channel declassification policy we introduce a further tradeoff between efficiency and verifiability: by writing programs in a particular ``manifest form'' security becomes considerably easier to verify.
|
|
