In this paper we're going to explore the ways in which security proofs can fail, and their broader lessons for security engineering. To mention just one example, Larry Paulson proved the security of SSL/TLS using his theorem prover Isabelle in 1999, yet it's sprung multiple leaks since then, from timing attacks to Heartbleed. We will go through a number of other examples in the hope of elucidating general principles. Proofs can be irrelevant, they can be opaque, they can be misleading and they can even be wrong. So we can look to the philosophy of mathematics for illumination. But the problem is more general. What happens, for example, when we have a choice between relying on mathematics and on physics? The security proofs claimed for quantum cryptosystems based on entanglement raise some pointed questions and may engage the philosophy of physics. And then there's the other varieties of assurance; we will recall the reliance placed on FIPS-140 evaluations, which API attacks suggested may have been overblown. Where the defenders focus their assurance effort on a subsystem or a model that cannot capture the whole attack surface they may just tell the attacker where to focus their effort. However, we think it's deeper and broader than that. The models of proof and assurance on which we try to rely have a social aspect, which we can try to understand from other perspectives ranging from the philosophy or sociology of science to the psychology of shared attention. These perspectives suggest, in various ways, how the management of errors and exceptions may be particularly poor. They do not merely relate to failure modes that the designers failed to consider properly or at all; they also relate to failure modes that the designers (or perhaps the verifiers) did not want to consider for institutional and cultural reasons.
A number of technology companies have introduced personal item tracking devices to allow people to locate and keep track of items such as keys and phones. However, these devices are not always used for their intended purpose: they have been used in cases of domestic abuse and stalking to track others without their consent. In response, manufacturers introduced a range of anti-stalking features designed to detect and mitigate misuse of their products. In this paper, we explore common implementations of these anti-stalking features and analyse their limitations. In other research, we identified that very few people use anti-stalking features, even when they know that someone might be tracking them and are incentivised to evade them. In this paper, we additionally identify several failures of the features that prevent them from performing their intended purpose even if they were in use. It is impossible for anti-stalking features to identify the difference between ‘bad’ tracking and ‘good’ tracking. Furthermore, some features work on some types of phones for some types of tracking devices, but not all work on all phones for all trackers. Some anti-stalking features are not enabled by default, and some require manual intervention to scan for devices. We provide suggestions for how these features could be improved, as well as ideas for additional anti-stalking features that could help mitigate the issues discussed in this paper.
Digital cash seems inevitable. But it’s not going to be bitcoin or the like, which will be regulated out of existence rather than being allowed to become mainstream currency. Central Bank Digital Currencies promise to eliminate crime but come with many of the problems that bitcoin set out to avoid. What do we actually need from digital cash? We had better figure it out before building and deploying unsuitable systems.
Although today’s most prevalent end-to-end encrypted messaging platforms using the Signal Protocol perform opportunistic encryption and provide resistance to eavesdropping, they are still vulnerable to impersonation attacks. We propose Trusted Introductions, a mechanism to transfer existing identity verifications between users, to increase resistance to active attacks. The proposal builds on the out-of-band user identity verification capabilities provided by the Signal Protocol. We argue that replacing user-managed identity-keys in cryptographic systems with the concept of an introduction, will increase users’ understanding and improve usability of the verification mechanism. Current events underscore the need for anonymous introductions, which can be achieved based on the Signal Protocol’s properties of forward secrecy and repudiation.
Keeping audit logs about past activities in any computer system is one of the requirements regulated decades ago. However, there is no clear definition of what information should be kept in audit logs. Therefore, most existing systems include identifiers in audit records that violate data privacy, or they apply pseudonymization techniques before logging that add unnecessary overhead to the system. In this paper, we define an auditing approach called blind auditing in which the audit logs contain just “enough” information to preserve data privacy and enable different auditing processes without adding intolerable overhead to the system being audited. With those blind audit logs, we define a probabilistic access control model that dynamically improves over time. Together, these allow auditing and access control that is performant, privacy-preserving and perpetually improving.
