Code-Level Protocol Verification

Abstract: Recent bugs in implementations, such as Heartbleed or in the Matrix chat application, demonstrate that formally verifying security properties for protocol models is an important first step but not enough to also guarantee them for implementations. We present a bottom-up verification approach to prove trace-based security properties directly on the level of existing implementations.

Machine readable specifications at scale

Abstract: There are lots of potential uses for machine readable specifications so you would think that every major real world artifact like long-lived hardware and software systems, protocols, languages, etc. would have a formal specification that is used by all teams extending, implementing, testing, verifying or securing the design. But, in practice, this is usually

Automating Cookie Consent and GDPR Violation Detection

Abstract: The European Union’s General Data Protection Regulation (GDPR) requires websites to inform users about personal data collection and request consent for cookies. Yet the majority of websites do not give users any choices, and others attempt to deceive them into accepting all cookies. We document the severity of this situation through an analysis of

WebGraph: Capturing Advertising and Tracking Information Flows for Robust Blocking

Abstract: Users rely on ad and tracker blocking tools to protect their privacy. Unfortunately, existing ad and tracker blocking tools are susceptible to mutable advertising and tracking content. In this paper, we first demonstrate that a state-of-the-art ad and tracker blocker, AdGraph, is susceptible to such adversarial evasion techniques that are currently deployed on the

LPGNet: Link Private Graph Networks for Node Classification

Abstract: Classification tasks on labeled graph-structured data have many important applications ranging from social recommendation to financial modeling. Deep neural networks are increasingly being used for node classification on graphs, wherein nodes with similar features have to be given the same label. Graph convolutional networks (GCNs) are one such widely studied neural network architecture that

Secure Ranging in 5G Wireless Networks

Abstract: A wide variety of applications, such as modern payment systems, access control for critical infrastructures, healthcare applications like contact tracing, depend on location and proximity information. There are multiple ways to establish physical distance between two entities, most of which are prone to distance modification attacks and can lead to loss of property (e.g.,

The Internet Computer

Abstract: I’ll give a demo of the Internet Computer which hosts powerful smart contracts that are general purpose, tamperproof, composable, autonomous and run at web speed. I’ll proceed with an overview of the platform, which is a sharded blockchain system which offers advanced features such as on-chain governance, scaling and system upgrades. Needless to say,