Publications
Contents |
Articles
-
Graeme Jenkinson, Lucian Carata, Thomas Bytheway, Ripduman Sohan, 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).
, , Brian Kidney, Amanda Strnad, and . [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, Clean Application Compartmentalization with SOAAP. CCS 2015: Proceedings of the 22nd ACM Conference on Computer and Communications Security, (2015).
, , Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann and and Alex Richardson. [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:
-
TESLA: Temporally Enhanced System Logic Assertions. EuroSys ’14: Proceedings of the Ninth European Conference on Computer Systems, (2014), 1–14.
, , , Khilan Gudka, Ilias Marinos and Brooks Davis. [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 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%}