Publications

Contents

Articles
Prior work

Articles

Graeme Jenkinson, Lucian Carata, Thomas Bytheway, Ripduman Sohan, Robert N. M. Watson, Jonathan Anderson, Brian Kidney, Amanda Strnad, Arun Thomas and George Neville-Neil. Applying Provenance in APT Monitoring and Analysis: Practical Challenges for Scalable, Efficient and Trustworthy Distributed Provenance. 9th USENIX Workshop on the Theory and Practice of Provenance (TaPP 2017), USENIX Association (2017). [BibTeX] [pdf]

{%raw%}@inproceedings{jenkinson2017apt,
  author = {Jenkinson, Graeme and Carata, Lucian and Bytheway, Thomas and Sohan, Ripduman and Watson, Robert N. M. and Anderson, Jonathan and Kidney, Brian and Strnad, Amanda and Thomas, Arun and Neville-Neil, George},
  title = {Applying Provenance in APT Monitoring and Analysis: Practical Challenges for Scalable, Efficient and Trustworthy Distributed Provenance},
  booktitle = {9th USENIX Workshop on the Theory and Practice of Provenance (TaPP 2017)},
  year = {2017},
  address = {Seattle, WA},
  pdf = {https://www.usenix.org/conference/tapp17/workshop-program/presentation/jenkinson},
  publisher = {USENIX Association}
}
{%endraw%}

Khilan Gudka, Robert N.M. Watson, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann and and Alex Richardson. Clean Application Compartmentalization with SOAAP. CCS 2015: Proceedings of the 22nd ACM Conference on Computer and Communications Security, (2015). [BibTeX] [pdf] [doi]

{%raw%}@inproceedings{gudka2015soaap,
  author = {Gudka, Khilan and Watson, Robert N.M. and Anderson, Jonathan and Chisnall, David and Davis, Brooks and Laurie, Ben and Marinos, Ilias and Neumann, Peter G. and and Alex Richardson},
  title = {{Clean Application Compartmentalization with SOAAP}},
  booktitle = {{CCS 2015: Proceedings of the 22nd ACM Conference on Computer and Communications Security}},
  city = {Denver},
  state = {CO},
  country = {USA},
  month = oct,
  year = {2015},
  pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2015ccs-soaap.pdf},
  doi = {http://dx.doi.org/10.1145/2810103.2813611}
}
{%endraw%}

Prior work

Prior work by members of the CADETS project that is of relevance includes:

Jonathan Anderson, Robert N. M. Watson, David Chisnall, Khilan Gudka, Ilias Marinos and Brooks Davis. TESLA: Temporally Enhanced System Logic Assertions. EuroSys ’14: Proceedings of the Ninth European Conference on Computer Systems, (2014), 1–14. [BibTeX] [abstract] [pdf] [doi]
```
{%raw%}@article{Anderson2014a,
  author = {Anderson, Jonathan and Watson, Robert N. M. and Chisnall, David and Gudka, Khilan and Marinos, Ilias and Davis, Brooks},
  title = {TESLA: Temporally Enhanced System Logic Assertions},
  booktitle = {EuroSys '14: Proceedings of the Ninth European Conference on Computer Systems},
  year = {2014},
  isbn = {978-1-4503-2704-6},
  pages = {1--14},
  location = {Amsterdam, The Netherlands},
  doi = {http://doi.acm.org/10.1145/2592798.2592801},
  publisher = {ACM},
  address = {New York, NY, USA},
  pdf = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201404-eurosys2014-tesla.pdf}
}
{%endraw%}
```
Large, complex, rapidly evolving pieces of software such as operating systems are notoriously difficult to prove correct. Developers instead describe expected behaviour through assertions and check actual behaviour through testing. However, many dynamic safety properties cannot be validated this way as they are temporal: they depend on events in the past or future and are not easily expressed in assertions.

TESLA is a description, analysis, and validation tool that allows systems programmers to describe expected temporal behaviour in low-level languages such as C. Temporal assertions can span the interfaces between libraries and even languages. TESLA exposes run-time behaviour using program instrumentation, illuminating coverage of complex state machines and detecting violations of specifications.

We apply TESLA to complex software, including an OpenSSL security API, the FreeBSD Mandatory Access Control framework, and GNUstep’s rendering engine. With performance allowing "always-on" availability, we demonstrate that existing systems can benefit from richer dynamic analysis without being re-written for amenability to a complete formal analysis.

Marshall Kirk McKusick, George V. Neville-Neil and Robert N. M. Watson. Design and Implementation of the FreeBSD Operating System, 2nd Edition. Pearson Education, 2014. [BibTeX]

{%raw%}@book{mckusick2014freebsd,
  author = {McKusick, Marshall Kirk and Neville-Neil, George V. and Watson, Robert N. M.},
  title = {{Design and Implementation of the FreeBSD Operating System, 2nd Edition}},
  publisher = {Pearson Education},
  city = {Boston},
  state = {MA},
  country = {USA},
  month = sep,
  year = {2014}
}
{%endraw%}

Brooks Davis. CheriBSD: a research fork of FreeBSD. . [BibTeX] [pdf]

{%raw%}@misc{Davis,
  author = {Davis, Brooks},
  mendeley-groups = {CADETS},
  title = {{CheriBSD: a research fork of FreeBSD}},
  howpublished = {https://www.bsdcan.org/2015/schedule/attachments/317\_BSDCan-CheriBSD.pdf},
  url = {https://www.bsdcan.org/2015/schedule/attachments/317\_BSDCan-CheriBSD.pdf},
  urldate = {2015-07-17}
}
{%endraw%}