topic.secure_encapsulation.bib

@comment{{This file has been generated by bib2bib 1.99}}

@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"secure_encapsulation" -ob topic.secure_encapsulation.bib sewellbib2.bib}}

@techreport{SV99a,
  author = {Peter Sewell and Jan Vitek},
  title = {Secure Composition of Insecure Components},
  institution = {Computer Laboratory, University of Cambridge},
  year = {1999},
  optkey = {},
  opttype = {},
  number = {UCAM-CL-TR-463},
  optaddress = {},
  month = apr,
  note = {44pp. },
  optannote = {},
  url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-463.html},
  pdf = {http://www.cl.cam.ac.uk/~pes20/wrap-tr.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/wrap-tr.ps},
  abstract = {Software systems are becoming heteroheneous: 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 infaesible to verify that such components are well-behaved. Instead they must be executed in a secure environment, or wrapper, that provides fine-grain control of the allowable interactions between them, and between components and other system resources.

In this paper we study such wrappers, focussing on how they can be expressed in a way that enables their security properties to be stated and proved rigorously. We introduce a model programming language, the box-$\pi$ calculus, that supports composition of software components and the enforcement of security policies. Several example wrappers are expressed using the calculus; we explore the delicate security properties they guarantee.},
  topic = {secure_encapsulation}
}

@inproceedings{SV99b,
  author = {Peter Sewell and Jan Vitek},
  title = {Secure Composition of Insecure Components},
  conf = {CSFW 1999},
  booktitle = {Proceedings of  the 12th IEEE Computer Security Foundations Workshop (Mordano)},
  optcrossref = {},
  optkey = {},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  year = {1999},
  optorganization = {},
  publisher = {IEEE Computer Society},
  optaddress = {},
  month = jun,
  pages = {136--150},
  note = {},
  optannote = {},
  url = {https://doi.org/10.1109/CSFW.1999.779769},
  doi = {10.1109/CSFW.1999.779769},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/wrap-csfw.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/wrap-csfw.ps},
  workshopurl = {http://www2.csl.sri.com/csfw/},
  abstract = {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, or wrapper, that
provides fine-grain control of the allowable interactions between them, and between components and other system resources.
In this paper we study such wrappers, focusing on how
they can be expressed in a way that enables their security
properties to be stated and proved rigorously. We introduce
a model programming language, the box-pi calculus, that
supports composition of software components and the enforcement of security policies. Several example wrappers
are expressed using the calculus; we explore the delicate
security properties they guarantee.
},
  topic = {secure_encapsulation}
}

@techreport{SV99c,
  author = {Peter Sewell and Jan Vitek},
  title = {Secure Composition of Untrusted Code:
Wrappers and Causality Types},
  institution = {Computer Laboratory, University of Cambridge},
  year = {1999},
  optkey = {},
  opttype = {},
  number = {UCAM-CL-TR-478},
  optaddress = {},
  month = nov,
  note = {36pp. },
  pdf = {http://www.cl.cam.ac.uk/~pes20/wraptypes-tr.pdf},
  ps = {http://www.cl.cam.ac.uk/~pes20/wraptypes-tr.ps},
  url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-478.html},
  abstract = {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. In previous work we introduced the box-π process calculus with constrained interaction to express wrappers and discussed the rigorous formulation of their security properties. This paper addresses the verification of wrapper information flow properties. 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 a unidirectional-flow wrapper enforces a causal flow property.},
  topic = {secure_encapsulation}
}

@inproceedings{SV00a,
  author = {Peter Sewell and Jan Vitek},
  title = {Secure Composition of Untrusted Code: Wrappers and Causality Types},
  conf = {CSFW 2000},
  booktitle = {Proceedings of the 13th IEEE Computer Security Foundations Workshop (Cambridge)},
  optcrossref = {},
  optkey = {},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  year = {2000},
  optorganization = {},
  publisher = {IEEE Computer Society},
  optaddress = {},
  month = jul,
  pages = {269--284},
  note = {},
  optannote = {},
  url = {https://doi.org/10.1109/CSFW.2000.856943},
  doi = {10.1109/CSFW.2000.856943},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/wraptypes.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/wraptypes.ps},
  abstract = {
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. In previous work
we introduced the box-$\pi$ process calculus with constrained
interaction to express wrappers and discussed the rigorous
formulation of their security properties. This paper addresses the verification of wrapper information flow properties. We present a novel causal type system that statically captures the allowed flows between wrapped possiblybadly-typed components; we use it to prove that an example
unidirectional-flow wrapper enforces a causal flow property.
},
  topic = {secure_encapsulation}
}

@article{SV-jcs,
  author = {Peter Sewell and Jan Vitek},
  title = {Secure Composition of Untrusted Code: Box-$\pi$, Wrappers and Causality Types},
  journal = {Journal of Computer Security},
  year = {2003},
  optkey = {},
  volume = {11},
  number = {2},
  optmonth = {},
  pages = {135-188},
  note = {Invited submission for a CSFW 00 special issue.},
  optannote = {},
  url = {http://content.iospress.com/articles/journal-of-computer-security/jcs165},
  pdf = {http://www.cl.cam.ac.uk/users/pes20/wrapall.pdf},
  ps = {http://www.cl.cam.ac.uk/users/pes20/wrapall.ps},
  abstract = {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-ss 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.
},
  topic = {secure_encapsulation}
}