| 1. |
- Askarov, Aslan, 1981, et al.
(författare)
-
Cryptographically-Masked Flows
- 2006
-
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. - 9783540377566 ; 4134, s. 353-369
-
Konferensbidrag (refereegranskat)abstract
- Cryptographic operations are essential for many security-critical systems. Reasoning about information flow in such systems is challenging because typical (noninterference-based) information-flow definitions allow no flow from secret to public data. Unfortunately, this implies that programs with encryption are ruled out because encrypted output depends on secret inputs: the plaintext and the key. However, it is desirable to allow flows arising from encryption with secret keys provided that the underlying cryptographic algorithm is strong enough. In this paper we conservatively extend the noninterference definition to allow safe encryption, decryption, and key generation. To illustrate the usefulness of this approach, we propose (and implement) a type system that guarantees noninterference for a small imperative language with primitive cryptographic operations. The type system prevents dangerous program behavior (e.g., giving away a secret key or confusing keys and non-keys), which we exemplify with secure implementations of cryptographic protocols. Because the model is based on a standard noninterference property, it allows us to develop some natural extensions. In particular, we consider public-key cryptography and integrity, which accommodate reasoning about primitives that are vulnerable to chosen-ciphertext attacks.
|
|
| 2. |
- Askarov, Aslan, 1981, et al.
(författare)
-
Cryptographically-Masked Flows
- 2008
-
Ingår i: Theoretical Computer Science. - : Elsevier BV. - 0304-3975. ; 402:2-3, s. 82-101
-
Tidskriftsartikel (refereegranskat)abstract
- Cryptographic operations are essential for many security-critical systems. Reasoning about information flow in such systems is challenging because typical (noninterference-based) information-flow definitions allow no flow from secret to public data. Unfortunately, this implies that programs with encryption are ruled out because encrypted output depends on secret inputs: the plaintext and the key. However, it is desirable to allow flows arising from encryption with secret keys provided that the underlying cryptographic algorithm is strong enough. In this article we conservatively extend the noninterference definition to allow safe encryption, decryption, and key generation. To illustrate the usefulness of this approach, we propose (and implement) a type system that guarantees noninterference for a small imperative language with primitive cryptographic operations. The type system prevents dangerous program behavior (e.g., giving away a secret key or confusing keys and nonkeys), which we exemplify with secure implementations of cryptographic protocols. Because the model is based on a standard noninterference property, it allows us to develop some natural extensions. In particular, we consider public-key cryptography and integrity, which accommodate reasoning about primitives that are vulnerable to chosen-ciphertext attacks.
|
|
| 3. |
|
|
| 4. |
- Gedell, Tobias, 1980, et al.
(författare)
-
Abstract Interpretation Plugins for Type Systems
- 2008
-
Ingår i: Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Urbana, IL, USA, July 28-31, 2008, Proceedings. - 9783540799795 ; LNCS 5140, s. 184-198
-
Konferensbidrag (refereegranskat)
|
|
| 5. |
|
|
| 6. |
- Hedin, Daniel, 1978
(författare)
-
Language Based Covert Channel Avoidance
- 2007
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)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 by accident or malice. Protecting the access to information is not enough to solve this problem. We have to ensure that the program uses the information in a secure way.Work on information flow security often ignores information flows through covert channels even though they pose a serious threat. In the first paper we present a framework for timing-aware information-flow type systems for a low-level language similar to a non-trivial subset of a sequential Java bytecode. The framework is parametrised over a 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. This gives us the possibility to easily experiment with different time models. We argue that this is important for two reasons:1) different applications may have different thresholds for what is an acceptable covert channel, and2) different implementations of the same language may contain different possibilities of covert channels.In the second paper we investigate a threat to practical information flow security: the failure to include the runtime environment of a language into consideration.It is important that the assumptions that are made in the study of the core language are honoured by the runtime system, in which inevitably every program will be run.In particular, the second paper studies one commonly made assumption in analyses of Java that may be broken by the runtime environment: 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 practise. For example, various important operations in Java's standard API, such as hashcodes or serialisation, might break pointer opacity. As a result, static information-flow analyses, which assume pointer opacity risk being unsound in practise, since the pointer representation provides an unchecked implicit leak --- a covert channel via the state of the memory allocator. 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.
|
|
| 7. |
- 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.
|
|
| 8. |
|
|
| 9. |
- 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.
|
|
| 10. |
|
|
