Journal of Computer Security

Software systems are becoming heterogeneous: instead of a small number of large programs from well-established sources, a user's desktop may now consist of many smaller components that interact in intricate ways. Some components will be downloaded from the network from sources that are only partially trusted. A user would like to know that a number of security properties hold, e.g., that personal data is not leaked to the net, but it is typically infeasible to verify that such components are well-behaved. Instead, they must be executed in a secure environment that provides fine-grain control of the allowable interactions between them, and between components and other system resources.

In this paper, we consider the problem of assembling concurrent software systems from untrusted or partially trusted off-the-shelf components, using wrapper programs to encapsulate components and enforce security policies. We introduce a model programming language, the box-π calculus, that supports composition of software components and the enforcement of information flow security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee. We present a novel causal type system that statically captures the allowed flows between wrapped possibly-badly-typed components; we use it to prove that an example ordered pipeline wrapper enforces a causal flow property.

We describe a verification method for cryptographic protocols, based on first-order invariants. For typical protocols, a suitable invariant can be generated mechanically from the program text, allowing safety properties to be proved by ordinary first-order reasoning.

The method has been implemented in an automatic verifier, TAPS, that proves safety properties comparable to those in published Isabelle verifications, but does so much faster with little or no guidance from the user. TAPS has verified properties of about 100 protocols, including all but three protocols from the Clark and Jacob survey; on average, these verifications require less than a second of CPU time and less than 4 bytes of hints from the user.

A type flaw attack on a security protocol is an attack where a field that was originally intended to have one type is subsequently interpreted as having another type. A number of type flaw attacks have appeared in the academic literature. In this paper we prove that type flaw attacks can be prevented using a simple technique of tagging each field with some information indicating its intended type.

In this paper we develop a language of mobile agents called uPLAN for describing the capabilities of active (programmable) networks. We use a formal semantics for uPLAN to demonstrate how capabilities provided for programming the network can affect the potential flows of information between users. In particular, we formalize a concept of security against attacks on secrecy by an ‘outsider’ and show how basic protections are preserved in the presence of programmable network functions.