The software supply chain is an increasingly common attack vector for malicious actors. The Node.js ecosystem has been subject to a wide array of attacks, likely due to its size and prevalence. To counter such attacks, the research community and practitioners have proposed a range of static and dynamic mechanisms, including process- and language-level sandboxing, permission systems, and taint tracking. Drawing on valuable insight from these works, this paper studies a runtime protection mechanism for (the supply chain of) Node.js applications with the ambitious goals of compatibility, automation, minimal overhead, and policy conciseness.

Software-Defined Networking (SDN) has transformed network architectures by decoupling the control and data-planes, enabling fine-grained control over packet processing and forwarding. P4, a language designed for programming data-plane devices, allows developers to define custom packet processing behaviors directly on programmable network devices. This provides greater control over packet forwarding, inspection, and modification. However, the increased flexibility provided by P4 also brings significant security challenges, particularly in managing sensitive data and preventing information leakage within the data-plane. This paper presents a novel security type system for analyzing information flow in P4 programs that combines security types with interval analysis. The proposed type system allows the specification of security policies in terms of input and output packet bit fields rather than program variables. We formalize this type system and prove it sound, guaranteeing that well-typed programs satisfy noninterference. Our prototype implementation, TAP4S, is evaluated on several use cases, demonstrating its effectiveness in detecting security violations and information leakages.

Automation apps enable seamless connection of IoT devices and services to provide useful functionality for end-users. Apps are typically executed on cloud-based Trigger-Action Platforms (TAPs) such as IFTTT and Node-RED, supporting both single- and multi-tenant models. Such models raise security and privacy concerns in the face of cloud attackers and malicious app makers, resulting in massive and uncontrolled exfiltration of sensitive user data.To address these concerns, we design TAPShield, an architecture that uses confidential computing and language-level sandboxing to protect user data against untrustworthy TAPs and malicious apps. TAPShield targets JavaScript-driven TAPs built on the Node.js environment and uses trusted execution environments implemented with Intel SGX to protect against cloud attackers. It further uses language-level sandboxes such as vm2 and SandTrap to protect against malicious apps. We implement TAPShield for two popular TAPs, Node-RED and IFTTT, and report on the security, performance, and compatibility trade-offs on a range of real-world apps. Our results show clear security benefits with acceptable performance overhead, while adhering to existing development practices of production-scale TAPs.

Computation over sensitive data requires that the computation function is secure and trusted. Existing approaches either do not enforce formal verification, require the user to verify the proof, or lack secure attestation guarantees. In addition, neither addresses the issue of having users once again inspect the application after upgrading the code running in the enclave. We propose an approach that uses a formal specification to guarantee that the behavior of the computation function conforms to the desired functionality. By combining automated verification with attestation on a trusted execution environment, we ensure that only conformant applications are executed. At the same time, we allow updates of the computation function without changing the attestation response, as long as the formal specification still holds. We implement and evaluate the system on several functions; our results show an average overhead of only 50 %. Finally, we demonstrate the validity of the system using a real-world application, Dafny-EVM.

When specifying security policies for databases, it is often natural to formulate disjunctive dependencies, where a piece of information may depend on at most one of two dependencies$P_{1}$or$P_{2}$, but not both. A formal semantic model of such disjunctive dependencies, the Quantale of Information, was recently introduced by Hunt and Sands as a generalization of the Lattice of Information. In this paper, we seek to contribute to the understanding of disjunctive dependencies in database-backed programs and introduce a practical framework to statically enforce disjunctive security policies. To that end, we introduce the Determinacy Quantale, a new query-based structure which captures the ordering of disjunctive information in databases. This structure can be understood as a query-based counterpart to the Quantale of Information. Based on this structure, we design a sound enforcement mechanism to check disjunctive policies for database-backed programs. This mechanism is based on a type-based analysis for a simple imperative language with database queries, which is precise enough to accommodate a variety of row-and column-level database policies flexibly while keeping track of disjunctions due to control flow. We validate our mechanism by implementing it in a tool, Divert, and demonstrate its feasibility on a number of use cases.

We introduce a framework for reasoning about the security of computer systems using modal logic. This framework is sufficiently expressive to capture a variety of known security properties, while also being intuitive and independent of syntactic details and enforcement mechanisms. We show how to use our formalism to represent various progress- and termination-(in)sensitive variants of confidentiality, integrity, robust declas-sification and transparent endorsement, and prove equivalence to standard definitions. The intuitive nature and closeness to semantic reality of our approach allows us to make explicit several hidden assumptions of these definitions, and identify potential issues and subtleties with them, while also holding the promise of formulating cleaner versions and future extension to entirely novel properties.

Smart home devices collect and transmit user data to smart home Trigger Action Platforms (TAPs) for processing and executing automation rules. However, this data can also be used to infer user activities or other sensitive information. In this paper, we propose PTAP, a privacy-preserving approach based on adversarial example attacks. PTAP injects targeted perturbations into time-series sensor data, effectively confounding potentially malicious TAP classifiers. Our approach significantly reduces the chance of user activity recognition for a malicious TAP while preserving the essential information for automation rule execution, thus safeguarding TAP utility. We evaluated PTAP using a real-world smart-home dataset and examined its effectiveness in preserving utility through the execution of various IoT applications. Our results demonstrate that PTAP effectively preserves user privacy (reducing the accuracy of a malicious classifier 91 to 6 percent) while maintaining automation rule integrity, providing a practical and effective solution to protect user privacy in smart-home environments.

Prototype-based languages like JavaScript are susceptible to prototype pollution vulnerabilities, enabling an attacker to inject arbitrary properties into an object's prototype. The attacker can subsequently capitalize on the injected properties by executing otherwise benign pieces of code, so-called gadgets, that perform security-sensitive operations. The success of an attack largely depends on the presence of gadgets, leading to high-profile exploits such as privilege escalation and arbitrary code execution (ACE).

Information flow control and dynamic policies is a difficult relationship yet to be fully understood. While dynamic policies are a natural choice in many real-world applications that downgrade and upgrade the sensitivity of information, understanding the meaning of security in this setting is challenging. In this paper we revisit the knowledge-based security conditions to reinstate a simple and intuitive security condition for dynamic policies: A program is secure if at any point during the execution the attacker's knowledge is in accordance with the active security policy at that execution point. Our key observation is the new notion of policy consistency to prevent policy changes whenever an attacker is already in possession of the information that the new policy intends to protect. We use this notion to study a range of realistic attackers including the perfect recall attacker, bounded attackers, and forgetful attackers, and their relationship. Importantly, our new security condition provides a clean connection between the dynamic policy and the underlying attacker model independently of the specific use case. We illustrate this by considering the different facets of dynamic policies in our framework. On the verification side, we design and implement DynCoVer, a tool for checking dynamic information-flow policies for Java programs via symbolic execution and SMT solving. Our verification operates by first extracting a graph of program dependencies and then visiting the graph to check dynamic policies for a range of attackers. We evaluate the effectiveness and efficiency of DyncoVeron a benchmark of use cases from the literature and designed by ourselves, as well as the case study of a social network. The results show that DynCoVer can analyze small but intricate programs indicating that it can help verify security-critical parts of Java applications. We release Dyncover publicly to support open science and encourage researchers to explore the topic further.

Confidential computing is a promising technology for securing code and data-in-use on untrusted host machines, e.g., the cloud. Many hardware vendors offer different implementations of Trusted Execution Environments (TEEs). A TEE is a hardware protected execution environment that allows performing confidential computations over sensitive data on untrusted hosts. Despite the appeal of achieving strong security guarantees against low-level attackers, two challenges hinder the adoption of TEEs. First, developing software in high-level managed languages, e.g., Java or Scala, taking advantage of existing TEEs is complex and error-prone. Second, partitioning an application into components that run inside and outside a TEE may break application-level security policies, resulting in an insecure application when facing a realistic attacker. In this work, we study both these challenges. We present JE, a programming model that seamlessly integrates a TEE, abstracting away low-level programming details such as initialization and loading of data into the TEE. JE only requires developers to add annotations to their programs to enable the execution within the TEE. Drawing on information flow control, we develop a security type system that checks confidentiality and integrity policies against realistic attackers with full control over the code running outside the TEE. We formalize the security type system for the JE core and prove it sound for a semantic characterization of security. We implement JE and the security type system, enable Java programs to run on Intel SGX with strong security guarantees. We evaluate our approach on use cases from the literature, including a battleship game, a secure event processing system, and a popular processing framework for big data, showing that we correctly handle complex cases of partitioning, information flow, declassification, and trust.

IoT systems, such as in smart cities or hospitals, generate data that may be subject to different security classifications, privacy regulations, and access rights. However, popular IoT platforms do not consider data classification and security-aware data analysis. In this paper, we present a novel architecture based on open-source solutions that handles the issue of collecting and classifying data at the source and presents the data analysis to users at different authorization levels. Our architecture consists of three layers: a layer for exposing collected and classified data to a middleware, the middleware to handle storage and analysis of the data and expose it to a dashboard, and the dashboard responsible for authenticating users and visualizing data according to the users’ classification level. Our solution distinguishes itself by focusing on data classification rather than data collection, supporting fine-grained access control and declassification. Our implementation, using the Web of Things API, Node-RED and Grafana, demonstrates the security benefits of our design on use cases in the smart city and healthcare domains.

IoT platforms enable users to connect various smart devices and online services via reactive apps running on the cloud. These apps, often developed by third-parties, perform simple computations on data triggered by external information sources and actuate the results of computations on external information sinks. Recent research shows that unintended or malicious interactions between the different (even benign) apps of a user can cause severe security and safety risks. These works leverage program analysis techniques to build tools for unveiling unexpected interference across apps for specific use cases. Despite these initial efforts, we are still lacking a semantic framework for understanding interactions between IoT apps. The question of what security policy cross-app interference embodies remains largely unexplored. This article proposes a semantic framework capturing the essence of cross-app interactions in IoT platforms. The framework generalizes and connects syntactic enforcement mechanisms to bisimulation-based notions of security, thus providing a baseline for formulating soundness criteria of these enforcement mechanisms. Specifically, we present a calculus that models the behavioral semantics of a system of apps executing concurrently, and use it to define desirable semantic policies targeting the security and safety of IoT apps. To demonstrate the usefulness of our framework, we define and implement static analyses for enforcing cross-app security and safety, and prove them sound with respect to our semantic conditions. We also leverage real-world apps to validate the practical benefits of our tools based on the proposed enforcement mechanisms.

The recent Spectre attacks have demonstrated the fundamental insecurity of current computer microarchitecture. The attacks use features like pipelining, out-of-order and speculation to extract arbitrary information about the memory contents of a process. A comprehensive formal microarchitectural model capable of representing the forms of out-of-order and speculative behavior that can meaningfully be implemented in a high performance pipelined architecture has not yet emerged. Such a model would be very useful, as it would allow the existence and non-existence of vulnerabilities, and soundness of countermeasures to be formally established. This paper presents such a model targeting single core processors. The model is intentionally very general and provides an infrastructure to define models of real CPUs. It incorporates microarchitectural features that underpin all known Spectre vulnerabilities. We use the model to elucidate the security of existing and new vulnerabilities, as well as to formally analyze the effectiveness of proposed countermeasures. Specifically, we discover three new (potential) vulnerabilities, including a new variant of Spectre v4, a vulnerability on speculative fetching, and a vulnerability on out-of-order execution, and analyze the effectiveness of existing countermeasures including constant time and serializing instructions.

Timing leaks have been a major concern for the security community. A common approach is to prevent secrets from affecting the execution time, thus achieving security with respect to a strong, local attacker who can measure the timing of program runs. However, this approach becomes restrictive as soon as programs branch on a secret. This paper focuses on timing leaks under remote execution. A key difference is that the remote attacker does not have a reference point of when a program run has started or finished, which significantly restricts attacker capabilities. We propose an extensional security characterization that captures the essence of remote timing attacks. We identify patterns of combining clock access, secret branching, and output in a way that leads to timing leaks. Based on these patterns, we design Clockwork, a monitor that rules out remote timing leaks. We implement the approach for JavaScript, leveraging JSFlow, a state-of-the-art information flow tracker. We demonstrate the feasibility of the approach on case studies with IFTTT, a popular IoT app platform, and VJSC, an advanced JavaScript library for e-voting.

IoT platforms enable users to connect various smart devices and online services via reactive apps running on the cloud. These apps, often developed by third-parties, perform simple computations on data triggered by external information sources and actuate the results of computation on external information sinks. Recent research shows that unintended or malicious interactions between the different (even benign) apps of a user can cause severe security and safety risks. These works leverage program analysis techniques to build tools for unveiling unexpected interference across apps for specific use cases. Despite these initial efforts, we are still lacking a semantic framework for understanding interactions between IoT apps. The question of what security policy cross-app interference embodies remains largely unexplored. This paper proposes a semantic framework capturing the essence of cross-app interactions in IoT platforms. The framework generalizes and connects syntactic enforcement mechanisms to bisimulation-based notions of security, thus providing a baseline for formulating soundness criteria of these enforcement mechanisms. Specifically, we present a calculus that models the behavioral semantics of a system of apps executing concurrently, and use it to define desirable semantic policies in the security and safety context of IoT apps. To demonstrate the usefulness of our framework, we define static mechanisms for enforcing cross-app security and safety, and prove them sound with respect to our semantic conditions. Finally, we leverage real-world apps to validate the practical benefits of our policy framework.

Securing database-backed applications requires tracking information across the application program and the database together, since securing each component in isolation may still result in an overall insecure system. Current research extends language-based techniques with models capturing the database's behavior. This research, however, relies on simplistic database models, which ignore security-relevant features that may leak sensitive information. We propose a novel security monitor for database-backed applications. Our monitor tracks fine-grained dependencies between variables and database tuples by leveraging database theory concepts like disclosure lattices and query determinacy. It also accounts for a realistic database model that supports security-critical constructs like triggers and dynamic policies. The monitor automatically synthesizes program-level code that replicates the behavior of database features like triggers, thereby tracking information flows inside the database. We also introduce symbolic tuples, an efficient approximation of dependency-tracking over disclosure lattices. We implement our monitor for Scala programs and demonstrate its effectiveness on four case studies.

This paper presents a practical and formal approach to analyze security-centric information flow policies at the level of the design model. Specifically, we focus on data confidentiality and data integrity objectives. In its guiding principles, the approach is meant to be amenable for designers (e.g., software architects) that have very limited or no background in formal models, logics, and the like. To this aim, we provide an intuitive graphical notation, which is based on the familiar Data Flow Diagrams, and which requires as little effort as possible in terms of extra security-centric information the designer has to provide. The result of the analysis algorithm is the early discovery of design flaws in the form of violations of the intended security properties. The approach is implemented as a publicly available plugin for Eclipse and evaluated with four real-world case studies from publicly available literature.

IoT apps empower users by connecting a variety of otherwise unconnected services. These apps (or applets ) are triggered by external information sources to perform actions on external information sinks. We demonstrate that the popular IoT app platforms, including IFTTT (If This Then That), Zapier, and Microsoft Flow are susceptible to attacks by malicious applet makers, including stealthy privacy attacks to exfiltrate private photos, leak user location, and eavesdrop on user input to voice-controlled assistants. We study a dataset of 279,828 IFTTT applets from more than 400 services, classify the applets according to the sensitivity of their sources, and find that 30% of the applets may violate privacy. We propose two countermeasures for short- and longterm protection: access control and information flow control. For short-term protection, we suggest that access control classifies an applet as either exclusively private or exclusively public, thus breaking flows from private sources to sensitive sinks. For longterm protection, we develop a framework for information flow tracking in IoT apps. The framework models applet reactivity and timing behavior, while at the same time faithfully capturing the subtleties of attacker observations caused by applet output. We show how to implement the approach for an IFTTT-inspired setting leveraging state-of-the-art information flow tracking techniques for JavaScript based on the JSFlow tool and evaluate its effectiveness on a collection of applets.

Taint tracking is a popular security mechanism for tracking data-flow dependencies, both in high-level languages and at the machine code level. But despite the many taint trackers in practical use, the question of what, exactly, tainting means - what security policy item bodies - remains largely unexplored. We propose explicit secrecy, a generic framework capturing the essence of explicit flows, i.e., the data flows tracked by tainting. The framework is semantic, generalizing previous syntactic approaches to formulating soundness criteria of tainting. We demonstrate the usefulness of the framework by instantiating it with both a simple high-level imperative language and an idealized RISC machine. To further understanding of what is achieved by taint tracking tools, both dynamic and static, we obtain soundness results with respect to explicit secrecy for the tainting engine cores of a collection of popular dynamic and static taint trackers.

Low level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control flow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Information flow properties create additional complications: They are hyperproperties relating multiple executions, and the possibility of interrupts and concurrency, and use of devices and features like memory-mapped I/O requires a departure from the usual initial-state final-state account of noninterference. In this work we propose a novel approach to relational verification for machine code. Verification goals are expressed as equivalence of traces decorated with observation points. Relational verification conditions are propagated between observation points using symbolic execution, and discharged using first-order reasoning. We have implemented an automated tool that integrates with SMT solvers to automate the verification task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent format using the BAP toolset by means of a verified translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assembly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine.

We address the problem of program verification for information flow policies by means of symbolic execution and model checking. Noninterference-like security policies are formalized using epistemic logic. We show how the policies can be accurately verified using a combination of concolic testing and SMT solving. As we demonstrate, many scenarios considered tricky in the literature can be solved precisely using the proposed approach. This is confirmed by experiments performed with ENCOVER, a tool based on Java Path Finder and Z3, which we have developed for epistemic noninterference concolic verification.