Ben Laurie
Authored Publications
Sort By
Policy Transparency: Authorization Logic Meets General Transparency to Prove Software Supply Chain Integrity
Andrew Ferraiuolo
Razieh Behjati
ACM Workshop on Software Supply Chain Offensive Research and Ecosystem Defenses, Association for Computing Machinery (2022)
Preview abstract
Building reliable software is challenging because today’s software supply chains are built
and secured from tools and individuals from a broad range of organizations
with complex trust relationships.
In this setting, tracking the origin of each piece of software and understanding the security
and privacy implications of using it is essential. In this work we aim to secure software
supply chains by using verifiable policies in which the origin of information and the
trust assumptions are first-order concerns and abusive evidence is discoverable.
To do so, we propose Policy Transparency, a new paradigm in which
policies are based on authorization logic and all claims issued in this policy
language are made transparent by inclusion in a transparency log. Achieving this
goal in a real-world setting is non-trivial and to do so we propose a novel
software architecture called PolyLog. We find that this combination
of authorization logic and transparency logs is mutually beneficial --
transparency logs allow authorization logic claims to be widely available aiding
in discovery of abuse, and making claims interpretable
with policies allows misbehavior captured in the transparency logs to be
handled proactively.
View details
Towards making formal methods normal: meeting developers where they are
Alastair Reid
Shaked Flur
Luke Church
Maritza Johnson
HATRA 2020: Human Aspects of Types and Reasoning Assistants (to appear)
Preview abstract
Formal verification of software is a bit of a niche activity: it is only applied to the most safety-critical or security-critical software and it is typically only performed by specialized verification engineers. This paper considers whether it would be possible to increase adoption of formal methods by integrating formal methods with developers' existing practices and workflows.
We do not believe that widespread adoption will follow from making the prevailing formal methods argument that correctness is more important than engineering teams realize. Instead, our focus is on what we would need to do to enable programmers to make effective use of formal verification tools and techniques. We do this by considering how we might make verification tooling that both serves developers' needs and fits into their existing development lifecycle. We propose a target of two orders of magnitude increase in adoption within a decade driven by ensuring a positive `weekly cost-benefit' ratio for developer time invested.
View details
Expert and Non-Expert Attitudes towards (Secure) Instant Messaging
Sauvik Das
Iulia Ion
Twelfth Symposium on Usable Privacy and Security (SOUPS 2016), USENIX Association, Denver, CO, pp. 147-157
Preview abstract
In this paper, we present results from an online survey with 1,510 participants and an interview study with 31 participants on (secure) mobile instant messaging. Our goal was to uncover how much of a role security and privacy played in people's decisions to use a mobile instant messenger. In the interview study, we recruited a balanced sample of IT security experts and non-experts, as well as an equal split of users of mobile instant messengers that are advertised as being more secure and/or private (e.g., Threema) than traditional mobile IMs. Our results suggest that peer influence is what primarily drives people to use a particular mobile IM, even for secure/private IMs, and that security and privacy play minor roles.
View details
A taste of Capsicum: practical capabilities for UNIX
Robert N. M. Watson
Jonathan Anderson
Kris Kennaway
Communications of the ACM, 55(3) (2012), pp. 97-104
Preview abstract
Capsicum is a lightweight operating system (OS) capability and sandbox framework planned for inclusion in
FreeBSD 9. Capsicum extends, rather than replaces, UNIX
APIs, providing new kernel primitives (sandboxed capability mode and capabilities) and a userspace sandbox API.
These tools support decomposition of monolithic UNIX
applications into compartmentalized logical applications,
an increasingly common goal that is supported poorly by
existing OS access control primitives. We demonstrate our
approach by adapting core FreeBSD utilities and Google
View details
Capsicum: practical capabilities for UNIX
Robert N. M. Watson
Jonathan Anderson
Kris Kennaway
Proceedings of the 19th USENIX Security Symposium (2010)
Preview abstract
Capsicum is a lightweight operating system capabil-
ity and sandbox framework planned for inclusion in
FreeBSD 9. Capsicum extends, rather than replaces,
UNIX APIs, providing new kernel primitives (sandboxed
capability mode and capabilities) and a userspace sand-
box API. These tools support compartmentalisation of
monolithic UNIX applications into logical applications,
an increasingly common goal supported poorly by dis-
cretionary and mandatory access control. We demon-
strate our approach by adapting core FreeBSD utilities
and Google’s Chromium web browser to use Capsicum
primitives, and compare the complexity and robustness
of Capsicum with other sandboxing techniques.
View details
Access Control
Preview
Google, Inc. (2008)
Selective Disclosure
Ben Laurie (2007)
Preview abstract
Selective disclosure for the non-cryptographer.
View details
