Security and privacy (S&P) advice plays a crucial role in how people stay safe online. While prior work shows that the plethora of advice from varied sources makes it difficult for users to prioritize advice, the insights are primarily based on studies conducted in Western contexts. Other work shows that users outside the West have different S&P needs and thus, we cannot simply rely on advice curated in the West to generalize to the majority world - regions of Africa, Asia, Latin America, and the Middle East, where most of the world's population lives. We fill this gap by investigating S&P advice across nine majority world countries via 70 semi-structured interviews with local experts: cybercafe operators, tech repair specialists, and other community figures that people commonly rely on for tech support and S&P advice. We find that the advice provided by local experts in the majority world largely matches the advice they provide to their constituents and the advice from the West. However, we surface various significant barriers that hinder majority world users from implementing advice, including economic constraints, language barriers, and social friction from taking protective measures. Our findings further show how factors such as social norms and gender shape advice practices, e.g., by driving gendered advice-seeking. We discuss how S&P advice in the majority world can be improved and reflect on how the S&P community can better engage with local communities in conducting similar research.

PLAS provides a forum for exploring and evaluating the use of programming language and program analysis techniques for promoting security in the complete range of software systems, from compilers to machine-learned models and smart contracts. The workshop encourages proposals of new, speculative ideas, evaluations of new or known techniques in practical settings, and discussions of emerging threats and problems. It also host position papers that are radical, forward-looking, and lead to lively and insightful discussions influential to the future research at the intersection of programming languages and security. This year will mark the 20th edition of PLAS, which was first held in 2007 in San Diego. The workshop will host 2 keynote talks, by Limin Jia and Jan Reineke, and 5 paper presentations.

GitHub is one of the most widely used public code development platform. However, the code hosted publicly on the platform is vulnerable to commit spoofing that allows an adversary to introduce malicious code or commits into the repository by spoofing the commit metadata to indicate that the code was added by a legitimate user. The only defense that GitHub employs is the process of commit signing, which indicates whether a commit is from a valid source or not based on the keys registered by the users.

With the recent advent of exploits like Spectre and Meltdown, the mitigation of side-channel attacks has become an important concern for security researchers. In this paper, we focus on timing-based side channels introduced through conditional branching on secret information within programs. We introduce a language that allows a programmer to write conditionals branching on secrets within its syntax, but has a semantics that keeps execution time constant with respect to an adversary under an observationally equivalent memory. We differ from other approaches that use program analysis methods, opting instead to modify the operational semantics to enforce the necessary properties. We formalize the semantics for our language with timing leak mitigations in Rocq (previously, Coq) and prove that these semantics satisfy the property of timing-sensitive non-interference. Since our system describes a mitigation approach for timing leaks in a general high-level imperative language, we believe that our semantics can be used as a basis for compiler construction for other high-level imperative languages that seek to be safe from timing side channels.

Web applications often include third-party content to personalize a user's online experience. These scripts have unrestricted access to a user's private data stored in the browser's persistent storage, associated with the host page. Various mechanisms have been implemented to restrict access to these storage objects, however, the existing mechanisms provide an all-or-none access and do not work in scenarios where web applications need to allow controlled access to cookies and localstorage objects by third-party scripts. If some of these scripts behave maliciously, they can easily access and modify private user information that are stored in the browser objects. The goal of our work is to design a mechanism to enforce fine-grained control of persistent storage objects. We perform an empirical study of persistent storage access by third-party scripts on Tranco's top 10,000 websites and find that 89.84% of all cookie accesses, 90.98% of all localstorage accesses and 72.49% of IndexedDB accesses are done by third-party scripts. Our approach enforces least privilege access for third-party scripts on these objects to ensure their security by attaching labels to the storage objects that specify which domains are allowed to read from and write to these objects. We implement our approach on the Firefox browser and show that it effectively blocks scripts from other domains, which are not allowed access based on these labels, from accessing the storage objects. We show that our enforcement results in some functionality breakage in websites with the default settings, which can be fixed by correctly labeling the storage objects used by the third-party scripts.

The EU General Data Protection Regulation (GDPR) requires websites to facilitate the right to revoke consent from Web users. Prior works have examined consent management by auditing that user choices are correctly stored, and comparing cookies set upon acceptance versus rejection to assess compliance. While these studies measured compliance of consent with respect to the various consent requirements, no prior work has studied consent revocation on the Web. Therefore, it is unclear how difficult it is to revoke consent on the websites’ interfaces, and whether the revoked consent is properly stored and communicated behind the user interface. Our work aims to fill this gap by measuring compliance of consent revocation on the Web on Tranco’s top-200 websites. We found that 19.87% of websites make it difficult for users to revoke consent throughout different interfaces, 20.5% of websites require more effort than acceptance, and 2.48% do not provide consent revocation at all, thus violating EU legal requirements for valid consent. 57.5% websites do not delete the cookies after consent revocation enabling continuous illegal processing of users’ data. Further, we analyzed 281 websites implementing the IAB Europe Transparency & Consent Framework, and found 22 websites that store a positive consent despite user’s revocation. Surprisingly, we found that on 101 websites, third parties that have received consent upon user’s acceptance, are not informed of revocation, leading to the illegal processing of users’ data by such third parties according to EU laws. Our findings emphasize the need for improved legal compliance of consent revocation, and proper, consistent, and uniform implementation of revocation communication to third-parties.

Attackers can steal sensitive user information from web pages via third-party scripts. Prior work shows that secure multi-execution (SME) with declassification is useful for mitigating such attacks, but that attackers can leverage dynamic web features to declassify more than intended. The proposed solution of disallowing events from dynamic web elements to be declassified is too restrictive to be practical; websites that declassify events from dynamic elements cannot function correctly.

To prevent applications from leaking users' private data to attackers, researchers have developed runtime information flow control (IFC) mechanisms. Most existing approaches are either based on taint tracking or multi-execution, and the same technique is used to protect the entire application. However, today's applications are typically composed of multiple components from heterogenous and unequally trusted sources. The goal of this paper is to develop a framework to enable the flexible composition of IFC enforcement mechanisms. More concretely, we focus on reactive programs, which is an abstract model for event-driven programs including web and mobile applications. We formalize the semantics of existing IFC enforcement mechanisms with well-defined interfaces for composition, define knowledge-based security guarantees that can precisely quantify the effect of implicit leaks from taint tracking, and prove sound all composed systems that we instantiate the framework with. We identify requirements for future enforcement mechanisms to be securely composed in our framework. Finally, we implement a prototype in OCaml and compare the effects of different compositions.

The Noise protocol framework defines a succinct notation and execution framework for a large class of 59+ secure channel protocols, some of which are used in popular applications such as WhatsApp and WireGuard. We present a verified implementation of a Noise protocol compiler that takes any Noise protocol, and produces an optimized C implementation with extensive correctness and security guarantees. To this end, we formalize the complete Noise stack in F*, from the low-level cryptographic library to a high-level API. We write our compiler also in F*, prove that it meets our formal specification once and for all, and then specialize it on-demand for any given Noise protocol, relying on a novel technique called hybrid embedding. We thus establish functional correctness, memory safety and a form of side-channel resistance for the generated C code for each Noise protocol. We propagate these guarantees to the high-level API, using defensive dynamic checks to prevent incorrect uses of the protocol. Finally, we formally state and prove the security of our Noise code, by building on a symbolic model of cryptography in F*, and formally link high-level API security goals stated in terms of security levels to low-level cryptographic guarantees. Ours are the first comprehensive verification results for a protocol compiler that targets C code and the first verified implementations of any Noise protocol. We evaluate our framework by generating implementations for all 59 Noise protocols and by comparing the size, performance, and security of our verified code against other (unverified) implementations and prior security analyses of Noise.

The ACME certificate issuance and management protocol, standardized as IETF RFC 8555, is an essential element of the web public key infrastructure (PKI). It has been used by Let's Encrypt and other certification authorities to issue over a billion certificates, and a majority of HTTPS connections are now secured with certificates issued through ACME. Despite its importance, however, the security of ACME has not been studied at the same level of depth as other protocol standards like TLS 1.3 or OAuth. Prior formal analyses of ACME only considered the cryptographic core of early draft versions of ACME, ignoring many security-critical low-level details that play a major role in the 100 page RFC, such as recursive data structures, long-running sessions with asynchronous sub-protocols, and the issuance for certificates that cover multiple domains.

The risk posed by high-profile data breaches has raised the stakes for adhering to data access policies for many organizations, but the complexity of both the policies themselves and the applications that must obey them raises significant challenges. To mitigate this risk, fine-grained audit of access to private data has become common practice, but this is a costly, time-consuming, and error-prone process.We propose an approach for automating much of the work required for fine-grained audit of private data access. Starting from the assumption that the auditor does not have an explicit, formal description of the correct policy, but is able to decide whether a given policy fragment is partially correct, our approach gradually infers a policy from audit log entries. When the auditor determines that a proposed policy fragment is appropriate, it is added to the system's mechanized policy, and future log entries to which the fragment applies can be dealt with automatically. We prove that for a general class of attribute-based data policies, this inference process satisfies a monotonicity property which implies that eventually, the mechanized policy will comprise the full set of access rules, and no further manual audit is necessary. Finally, we evaluate this approach using a case study involving synthetic electronic medical records and the HIPAA rule, and show that the inferred mechanized policy quickly converges to the full, stable rule, significantly reducing the amount of effort needed to ensure compliance in a practical setting.

Information flow type systems enforce the security property of noninterference by detecting unauthorized data flows at compile-time. However, they require precise type annotations, making them difficult to use in practice as much of the legacy infrastructure is written in untyped or dynamically-typed languages. Gradual typing seamlessly integrates static and dynamic typing, providing the best of both approaches, and has been applied to information flow control, where information flow monitors are derived from gradual security types. Prior work on gradual information flow typing uncovered tensions between noninterference and the dynamic gradual guarantee- the property that less precise security type annotations in a program should not cause more runtime errors.This paper re-examines the connection between gradual information flow types and information flow monitors to identify the root cause of the tension between the gradual guarantees and noninterference. We develop runtime semantics for a simple imperative language with gradual information flow types that provides both noninterference and gradual guarantees. We leverage a proof technique developed for FlowML and reduce noninterference proofs to preservation proofs.

We present$\text{DY}^{\star}$, a new formal verification framework for the symbolic security analysis of cryptographic protocol code written in the$\mathrm{F}^{\star}$programming language. Unlike automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Our work extends a long line of research on using dependent type systems for this task, but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. This approach enables us to uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security.$\text{DY}^{\star}$is built as a library of$\mathrm{F}^{\star}$modules that includes a model of low-level protocol execution, a Dolev-Yao symbolic attacker, and generic security abstractions and lemmas, all verified using$\mathrm{F}^{\star}$. The library exposes a high-level API that facilitates succinct security proofs for protocol code. We demonstrate the effectiveness of this approach through a detailed symbolic security analysis of the Signal protocol that is based on an interoperable implementation of the protocol from prior work, and is the first mechanized proof of Signal to account for forward and post-compromise security over an unbounded number of protocol rounds.

Information flow control (IFC) has been extensively studied as an approach to mitigate information leaks in applications. A vast majority of existing work in this area is based on static analysis. However, some applications, especially on the Web, are developed using dynamic languages like JavaScript where static analyses for IFC do not scale well. As a result, there has been a growing interest in recent years to develop dynamic or runtime information flow analysis techniques. In spite of the advances in the field, runtime information flow analysis has not been at the helm of information flow security, one of the reasons being that the analysis techniques and the security property related to them (non-interference) over-approximate information flows (particularly implicit flows), generating many false positives. In this paper, we present a sound and precise approach for handling implicit leaks at runtime. In particular, we present an improvement and enhancement of the so-called permissive-upgrade strategy, which is widely used to tackle implicit leaks in dynamic information flow control. We improve the strategy’s permissiveness and generalize it. Building on top of it, we present an approach to handle implicit leaks when dealing with complex features like unstructured control flow and exceptions in higher-order languages. We explain how we address the challenge of handling unstructured control flow using immediate post-dominator analysis. We prove that our approach is sound and precise.

Database-backed applications rely on inlined policy checks to process users' private and confidential data in a policy-compliant manner as traditional database access control mechanisms cannot enforce complex policies. However, application bugs due to missed checks are common in such applications, which result in data breaches. While separating policy from code is a natural solution, many data protection policies specify restrictions based on the context in which data is accessed and how the data is used. Enforcing these restrictions automatically presents significant challenges, as the information needed to determine context requires a tight coupling between policy enforcement and an application's implementation.

Web browsers routinely handle private information. Owing to a lax security model, browsers and JavaScript in particular, are easy targets for leaking sensitive data. Prior work has extensively studied information flow control (IFC) as a mechanism for securing browsers. However, two central aspects of web browsers - the Document Object Model (DOM) and the event handling mechanism - have so far evaded thorough scrutiny in the context of IFC. This paper advances the state-of-the-art in this regard. Based on standard specifications and the code of an actual browser engine, we build formal models of both the DOM (up to Level 3) and the event handling loop of a typical browser, enhance the models with fine-grained taints and checks for IFC, prove our enhancements sound and test our ideas through an instrumentation of WebKit, an in-production browser engine. In doing so, we observe several channels for information leak that arise due to subtleties of the event loop and its interaction with the DOM.

Most web applications today use JavaScript for including third-party scripts, advertisements etc., which pose a major security threat in the form of confidentiality and integrity violations. Dynamic information flow control helps address this issue of information stealing. Most of the approaches over-approximate when unstructured control flow comes into picture, thereby raising a lot of false alarms. We utilize the post-dominator analysis technique to determine the context of the program at a given point and prove that this approach is the most precise technique to handle implicit flows.