Unpredictable costs are a growing concern in serverless computing, where applications rely on cloud APIs with complex tiered pricing models. In many deployments, API calls dominate expenses, and a single overlooked design choice can escalate costs by thousands of dollars. Existing tools fall short: provider calculators need unrealistic manual estimates, and dynamic profilers only work post-deployment.

SMT solvers are essential for applications in artificial intelligence, software verification, and optimisation. However, no single solver excels across all formula types, and different applications may require the use of different solvers. While the SMT-LIB language enables multi-solver support, it also incurs heavy I/O overhead. To address this, we introduce Smt.ml , an SMT-solver frontend for OCaml that simplifies integration with various solvers through a consistent interface. Its parametric encoding facilitates the easy addition of new solver backends, while optimisations like formula simplification, result caching, and detailed error feedback enhance performance and usability. Furthermore, Smt.ml is the only SMT frontend that includes a simplification-management engine for streamlining the integration of new formula simplifications and the verification of their correctness. Our evaluation demonstrates that Smt.ml ’s results are consistent with those of its backend solvers and that its optimisations are highly effective on formulas generated from the symbolic execution of an extensive program-analysis benchmark.

Large Language Models (LLMs) have found widespread applications in various domains, including web applications with chatbot interfaces. Aided by an LLM-integration middleware such as LangChain, user prompts are translated into SQL queries used by the LLM to provide meaningful responses to users. However, unsanitized user prompts can lead to SQL injection attacks, potentially compromising the security of the database. In this paper, we present a comprehensive examination of prompt-to-SQL ($\mathbf{P}_{2} \mathbf{S Q L}$) injections targeting web applications based on frameworks such as LangChain and LlamaIndex. We characterize$\mathrm{P}_{2} \text{SQL}$injections, exploring their variants and impact on application security through multiple concrete examples. We evaluate seven state-of-the-art LLMs, demonstrating the risks of$P_{2}$SQL attacks across language models. By employing both manual and automated methods, we discovered$\mathrm{P}_{2} \text{SQL}$vulnerabilities in five real-world applications. Our findings indicate that LLMintegrated applications are highly susceptible to$\mathrm{P}_{2} \text{SQL}$injection attacks, warranting the adoption of robust defenses. To counter these attacks, we propose four effective defense techniques that can be integrated as extensions to the LangChain framework.

Federated Learning traditionally relies on differential privacy or cryptographic techniques such as Secure Aggregation and Homomorphic Encryption to protect data during distributed training, but these approaches incur high computational and communication costs. The emergence of hardware-based Trusted Execution Environments, particularly Confidential Virtual Machines (CVMs), offers a practical alternative by enabling secure computation on untrusted cloud infrastructures without algorithmic changes.However, CVM deployments by cloud providers—Google Cloud, Microsoft Azure, and AWS—remain opaque, inconsistent, and difficult to reproduce. This paper analyzes their trust models, attestation mechanisms, and deployment limitations, and introduces EVIDENT, a unified framework for transparent CVM lifecycle management. Furthermore, it supports attested interaction scenarios in which CVMs execute workloads owned by third parties—such as confidential AI inference—under cryptographically verifiable trust conditions.

The Node.js ecosystem, with its growing popularity and increasing exposure to security vulnerabilities, has a pressing need for more effective security analysis tools. To reduce false positives, recent works on detecting vulnerabilities in Node.js packages have developed synthesis algorithms to generate proof-of-concept exploits. However, these tools focus mainly on vulnerabilities that can be triggered by a single direct call to an exported function of the analyzed package, failing to generate exploits that require more complex interactions. In this paper, we present Explode.js , the first tool capable of synthesizing exploits that include complex call sequences to trigger vulnerabilities in Node.js packages. By combining static analysis and symbolic execution, Explode.js generates functional exploits that confirm the existence of command, code injection, prototype pollution, and path traversal vulnerabilities, effectively eliminating false positives. The results of evaluating Explode.js on two state-of-the-art datasets of Node.js packages with confirmed vulnerabilities show that it generates significantly more exploits than its main competitor tools. Furthermore, when applied to real-world Node.js packages, Explode.js uncovered 44 zero-day vulnerabilities, with 4 new CVEs.

As the Internet evolves from TLS 1.2 to TLS 1.3, it offers enhanced security against network eavesdropping for online communications. However, this advancement also enables malicious command and control (C2) traffic to more effectively evade malware detectors and intrusion detection systems. Among other capabilities, TLS 1.3 introduces encryption for most handshake messages and conceals the actual TLS record content type, complicating the task for state-of-the-art C2 traffic classifiers that were initially developed for TLS 1.2 traffic. Given the pressing need to accurately detect malicious C2 communications, this paper examines to what extent existing C2 classifiers for TLS 1.2 are less effective when applied to TLS 1.3 traffic, posing a central research question: is it possible to adapt TLS 1.2 detection methodologies for C2 traffic to work with TLS 1.3 flows?

While static analysis tools that rely on Code Property Graphs (CPGs) to detect security vulnerabilities have proven effective, deciding how much information to include in the graphs remains a challenge. Including less information can lead to a more scalable analysis but at the cost of reduced effectiveness in identifying vulnerability patterns, potentially resulting in classification errors. Conversely, more information in the graph allows for a more effective analysis but may affect scalability. For example, scalability issues have been recently highlighted in ODGen, the state-of-the-art CPG-based tool for detecting Node.js vulnerabilities. This paper examines a new point in the design space of CPGs for JavaScript vulnerability detection. We introduce the Multiversion Dependency Graph (MDG), a novel graph-based data structure that captures the state evolution of objects and their properties during program execution. Compared to the graphs used by ODGen, MDGs are significantly simpler without losing key information needed for vulnerability detection. We implemented Graph.js, a new MDG-based static vulnerability scanner specialized in analyzing npm packages and detecting taint-style and prototype pollution vulnerabilities. Our evaluation shows that Graph.js outperforms ODGen by significantly reducing both the false negatives and the analysis time. Additionally, we have identified 49 previously undiscovered vulnerabilities in npm packages.

Pressured by existing regulations such as the EU GDPR, online services must advertise a personal data protection policy declaring the types and purposes of collected personal data, which must then be strictly enforced as per the consent decisions made by the users. However, due to the lack of system-level support, obtaining strong guarantees of policy enforcement is hard, leaving the door open for software bugs and vulnerabilities to cause GDPR-compliance violations.We present RuleKeeper, a GDPR-aware personal data policy compliance system for web development frameworks. Currently ported for the MERN framework, RuleKeeper allows web developers to specify a GDPR manifest from which the data protection policy of the web application is automatically generated and is transparently enforced through static code analysis and runtime access control mechanisms. GDPR compliance is checked in a cross-cutting manner requiring few changes to the application code. We used our prototype implementation to evaluate RuleKeeper with four real-world applications. Our system can model realistic GDPR data protection requirements, adds modest performance overheads to the web application, and can detect GDPR violation bugs.

With the emergence of the Node.js ecosystem, JavaScript has become a widely used programming language for implementing server-side web applications. In this article, we present the first empirical study of static code analysis tools for detecting vulnerabilities in Node.js code. To conduct a comprehensive tool evaluation, we created the largest known curated dataset of Node.js code vulnerabilities. We characterized and annotated a set of 957 vulnerabilities by analyzing information contained innpmadvisory reports. We tested nine different tools and found that many important vulnerabilities appearing in the OWASP top-10 are not detected by any tool. The three best performing tools combined only detect up to 57.6% of all vulnerabilities in the dataset, but at a very low precision of 0.11%. Our curated dataset offers a new benchmark to help characterize existing Node.js code vulnerabilities and foster the development of better vulnerability detection tools for Node.js code.

Several totalitarian states around the world deploy sophisticated censorship apparatuses to prevent citizens from freely accessing the Internet. To counter these restrictions, some censorship-circumven-tion tools establish covert channels through the media streams of popular conferencing applications. A recent tool named Protozoa allows for establishing high-performing, peer-to-peer covert channels over WebRTC media streams. However, Protozoa is vulnerable to potential man-in-the-middle attacks. This may occur in cases where WebRTC applications rely on WebRTC gateways to mediate users' connections. In such cases, an adversary that controls the WebRTC gateway can inspect the content of the media streams and trivially detect the transmission of covert payload.

Pressured by existing regulations such as the EU GDPR, online services must advertise a personal data protection policy declaring the types and purposes of collected personal data, which must then be strictly enforced as per the consent decisions made by the users. However, due to the lack of system-level support, obtaining strong guarantees of policy enforcement is hard, leaving the door open for software bugs and vulnerabilities to cause GDPR-compliance violations. We present ongoing work on building a GDPR-aware personal data policy compliance system for web development frameworks. Currently prototyped for the MERN framework, our system allows web developers to specify a GDPR manifest from which the data protection policy of the web application is automatically generated and is transparently enforced through static code analysis and runtime access control mechanisms. GDPR compliance is checked in a cross-cutting manner requiring few changes to the application code. We evaluate our prototype with four real-world applications. Our system can model realistic GDPR data protection requirements, adds modest performance overheads to the web application, and can detect GDPR violation bugs.

Tor is the most popular anonymity network in the world. It relies on advanced security and obfuscation techniques to ensure the privacy of its users and free access to the Internet. However, the investigation of traffic correlation attacks against Tor Onion Services (OSes) has been relatively overlooked in the literature. In particular, determining whether it is possible to emulate a global passive adversary capable of deanonymizing the IP addresses of both the Tor OSes and of the clients accessing them has remained, so far, an open question. In this paper, we present ongoing work toward addressing this question and reveal some preliminary results on a scalable traffic correlation attack that can potentially be used to deanonymize Tor OS sessions. Our attack is based on a distributed architecture involving a group of colluding ISPs from across the world. After collecting Tor traffic samples at multiple vantage points, ISPs can run them through a pipeline where several stages of traffic classifiers employ complementary techniques that result in the deanonymization of OS sessions with high confidence (i.e., low false positives). We have responsibly disclosed our early results with the Tor Project team and are currently working not only on improving the effectiveness of our attack but also on developing countermeasures to preserve Tor users' privacy.

WebAssembly (Wasm) is a new binary instruction format that allows targeted compiled code written in high-level languages to be executed by the browser’s JavaScript engine with near-native speed. Despite its clear performance advantages, Wasm opens up the opportunity for bugs or security vulnerabilities to be introduced into Web programs, as pre-existing issues in programs written in unsafe languages can be transferred down to cross-compiled binaries. The source code of such binaries is frequently unavailable for static analysis, creating the demand for tools that can directly tackle Wasm code. Despite this potentially security-critical situation, there is still a noticeable lack of tool support for analysing Wasm binaries. We present WASP, a symbolic execution engine for testing Wasm modules, which works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library for C and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; and was further tested against the Test-Comp benchmark, obtaining results comparable to well-established symbolic execution and testing tools for C.

Computation Storage Architectures (CSA) are increasingly adopted in the cloud for near data processing, where the underlying storage devices/servers are now equipped with heterogeneous cores which enable computation offloading near to the data. While CSA is a promising high-performance architecture for the cloud, in general data analytics also presents significant data security and policy compliance (e.g., GDPR) challenges in untrusted cloud environments. In this paper, we present IronSafe, a secure and policy-compliant query processing system for heterogeneous computational storage architectures, while preserving the performance advantages of CSA in untrusted cloud environments. To achieve these design properties in a computing environment with heterogeneous host (x86) and storage system (ARM), we design and implement the entire hardware and software system stack from the ground-up leveraging hardware-assisted Trusted Execution Environments (TEEs): namely, Intel SGX and ARM TrustZone. More specifically, IronSafe builds on three core contributions: (1) a heterogeneous confidential computing framework for shielded execution with x86 and ARM TEEs and associated secure storage system for the untrusted storage medium; (2) a policy compliance monitor to provide a unified service for attestation and policy compliance; and (3) a declarative policy language and associated interpreter for concisely specifying and efficiently evaluating a rich set of polices. Our evaluation using the TPC-H SQL benchmark queries and GDPR anti-pattern use-cases shows that IronSafe is faster, on average by 2.3x than a host-only secure system, while providing strong security and policy-compliance properties.

WebAssembly is a new binary instruction format that allows targeted compiled code written in high-level languages to be executed with near-native speed by the browser’s JavaScript engine. However, given that WebAssembly binaries can be compiled from unsafe languages like C/C++, classical code vulnerabilities such as buffer overflows or format strings can be transferred over from the original programs down to the cross-compiled binaries. As a result, this possibility of incorporating vulnerabilities in WebAssembly modules has widened the attack surface of modern web applications. This paper presents Wasmati, a static analysis tool for finding security vulnerabilities in WebAssembly binaries. It is based on the generation of a code property graph (CPG), a program representation previously adopted for detecting vulnerabilities in various languages but hitherto unapplied to WebAssembly. We formalize the definition of CPG for WebAssembly, introduce techniques to generate CPG for complex WebAssembly, and present four different query specification languages for finding vulnerabilities by traversing a program’s CPG. We implemented ten queries capturing different vulnerability types and extensively tested Wasmati on four heterogeneous datasets. We show that Wasmati can scale the generation of CPGs for large real-world applications and can efficiently find vulnerabilities for all our query types. We have also tested our tool on WebAssembly binaries collected in the wild and identified several potential vulnerabilities, some of which we have manually confirmed to exist unless the enclosing application properly sanitizes the interaction with such affected binaries.

Many censorship circumvention tools rely on trusted proxies that allow users within censored regions to access blocked Internet content by tunneling it through a covert channel (e.g,. piggybacking on Skype video calls). However, building tools that can simultaneously (i) provide good bandwidth capacity for accommodating the typical activities of Internet users, and (ii) be secure against traffic analysis attacks has remained an open problem and a stumbling block to the practical adoption of such tools for censorship evasion.

Smart home technology has gained widespread adoption. However, several instances of massive corporate surveillance and episodes of sensor data breaches have raised many privacy concerns amongst potential consumers. This paper presents PatrIoT, a private-by-design IoT platform for smart home environments. PatrIoT revisits the typical architecture of existing IoT platforms, and provides an alternative design where the home owner retains full ownership and control of smart device generated data. It leverages Intel SGX to prevent unauthorized access to the data by untrusted IoT cloud providers, and offers homeowners an intuitive security abstraction named flowwall which allows them to specify easy-to-use policies for controlling sensitive sensor data flows within their smart homes. We have built and evaluated a PatrIoT prototype. Most of the participants in a field study considered PatrIoT to be easy to use, and the supported policies to be useful in protecting their privacy.

Hundreds of millions of mobile devices worldwide rely on Trusted Execution Environments (TEEs) built with Arm TrustZone for the protection of security-critical applications (e.g., DRM) and operating system (OS) components (e.g., Android keystore). TEEs are often assumed to be highly secure; however, over the past years, TEEs have been successfully attacked multiple times, with highly damaging impact across various platforms. Unfortunately, these attacks have been possible by the presence of security flaws in TEE systems. In this paper, we aim to understand which types of vulnerabilities and limitations affect existing TrustZone-assisted TEE systems, what are the main challenges to build them correctly, and what contributions can be borrowed from the research community to overcome them. To this end, we present a security analysis of popular TrustZone-assisted TEE systems (targeting Cortex-A processors) developed by Qualcomm, Trustonic, Huawei, Nvidia, and Linaro. By studying publicly documented exploits and vulnerabilities as well as by reverse engineering the TEE firmware, we identified several critical vulnerabilities across existing systems which makes it legitimate to raise reasonable concerns about the security of commercial TEE implementations.

Software security is a fundamental dimension in the development of mobile applications (apps). Since many apps have access to sensitive data (e.g., collected from a smartphone's sensors), the presence of security vulnerabilities may put that data in danger and lead to privacy violations. Unfortunately, existing security solutions for Android are either too cumbersome to use by common app developers, or may require the modification of Android OS. This paper presents Flowverine, a system for building privacy-sensitive mobile apps for unmodified Android platforms. Flowverine exposes an API based on a dataflow programming model which allows for efficient taint tracking of sensitive data flows within each app. By checking such flows against a security policy, Flowverine can then prevent potential privacy violations. We implemented a prototype of our system. Our evaluation shows that Flowverine can be used to implement mobile applications that handle security-sensitive information flows while preserving compatibility with existing Android OS and incurring small performance overheads.

The increase of personal data on mobile devices has been followed by legislation that forces service providers to process and maintain users' data under strict data protection policies. In this paper, we propose a new primitive for mobile applications called auditable mobile function (AMF) to help service providers enforcing such policies by enabling them to process sensitive data within users' devices and collecting proofs of function execution integrity. We present SafeChecker, a computation verification system that provides mobile application support for AMFs, and evaluate the practicality of different usage scenario AMFs on TrustZone-enabled hardware.

In certain restrictive usage scenarios, personal mobile devices are required to operate in some constrained manner. Security concerns tend to be the most typical motivation, for example, as in "Bring Your Own Device" use cases. However, because most device configurations are strictly controlled by their respective users, today it is practically infeasible to satisfy such requirements. In this paper, we present TrUbi, a system that allows for dynamic and temporary restriction of Android devices by disabling or locking specific functions for limited amounts of time, e.g. network blocked. TrUbi enforces global security policies by implementing an OS primitive named trust lease. Our TrUbi prototype can efficiently enforce security policies in unmodified real-world apps and paves the way for new apps that are currently unsupported by existing mobile platforms.

Abstract This paper studies the possibility of using the encrypted video channel of widely used videoconferencing applications, such as Skype, as a carrier for unobservable covert TCP/IP communications. We propose and evaluate different alternatives to encode information in the video stream in order to increase available throughput while preserving the packet-level characteristics of the video stream. We have built a censorship-resistant system, named DeltaShaper, which offers a data-link interface and supports TCP/IP applications that tolerate low throughput / high latency links. Our results show that it is possible to run standard protocols such as FTP, SMTP, or HTTP over Skype video streams.

Platform-as-a-Service (PaaS) infrastructures are highly dependent on cloud administrators. Ill-configured software systems or compromising insider activity can result in serious data breaches for clients of PaaS services. A general security approach against untrusted administrators is to employ operating system hardening techniques to limit access privileges on cloud nodes. However, this approach is overly inflexible for PaaS services, since superuser privileges tend to be required to apply a security patch, change a firewall rule, etc. This paper presents P-Cop, a system aimed to provide secure PaaS maintenance while preserving administration flexibility. To that end, P-Cop implements a bipartite maintenance model in which cloud administrator privileges can be elevated to superuser on a given node, but no sensitive guest computations can be allocated to the node until the issued command sequence has been endorsed by an auditor, i.e., a third-party mutually trusted by cloud provider and clients. P-Cop relies on a trusted proxy which supervises all privileged commands issued by the cloud administrators. Our current P-Cop design targets Docker-containerized PaaS services and leverages TPM hardware to enable remote attestation by external clients.

Self-destructing messaging applications have garnered immense popularity due to the arrival of Snapchat. However, Snapchat's history has shown that building such services on modern mobile platforms is very challenging. In fact, either caused by programming errors or due to the limitations of existing mobile operating systems, in Snapchat and other similar applications it is possible to recover supposedly deleted messages against the senders' expectations, therefore leaving millions of users potentially vulnerable to privacy breaches. This paper presents ShareIff, a middleware for Android that provides an API for secure sharing and display of self-destructing messages. Using this middleware, Snapchat or any similar application, is able to encrypt the message on the sender's endpoint and send it to the recipient such that the message can be decrypted and securely displayed only on the recipient's device for the amount of time specified by the sender. ShareIff provides this property by relying on specialized cryptographic protocols and operating system mechanisms. ShareIff offers application developers a simple programming abstraction and adds marginal overheads to system and app.

Cloud storage services are currently a commodity that allows users to store data persistently, access the data from everywhere, and share it with friends or co-workers. However, due to the proliferation of cloud storage accounts and lack of interoperability between cloud services, managing and sharing cloud-hosted files is a nightmare for many users. To address this problem, specialized cloud aggregator systems emerged that provide users a global view of all files in their accounts and enable file sharing between users from different clouds. Such systems, however, have limited security: not only they fail to provide end-to-end privacy from cloud providers, but they require users to grant full access privileges to individual cloud storage accounts. In this paper, we present Storekeeper, a privacy-preserving cloud aggregation service that enables file sharing on multi-user multi-cloud storage platforms while preserving data confidentiality from cloud providers and from the cloud aggregator service. To provide this property, Storekeeper decentralizes most of the cloud aggregation logic to the client side enabling security sensitive functions to be performed only on the trusted client endpoints. This decentralization brings new challenges related with file update propagation, access control, user authentication, and key management that are addressed by Storekeeper. This is provided at a low cost (7% on average) when compared with the underlining cloud providers.

This paper presents the design, implementation, and evaluation of the Trusted Language Runtime (TLR), a system that protects the confidentiality and integrity of .NET mobile applications from OS security breaches. TLR enables separating an application's security-sensitive logic from the rest of the application, and isolates it from the OS and other apps. TLR provides runtime support for the secure component based on a .NET implementation for embedded devices. TLR reduces the TCB of an open source .NET implementation by a factor of $78$ with a tolerable performance cost. The main benefit of the TLR is to bring the developer benefits of managed code to trusted computing. With the TLR, developers can build their trusted components with the productivity benefits of modern high level languages, such as strong typing and garbage collection.

The Internet is witnessing explosive growth in traffic due to bulk content transfers, such as multimedia and software downloads, and online sharing of personal, commercial, and scientific data. Yet bulk data transfers remain very expensive and inefficient. As a result, huge amounts of digital data continue to be delivered outside of the Internet using hard drives, optical media or tapes. Meanwhile, large reserves of spare bandwidth lie unutilized in today's networks, where links are overprovisioned for peak load. We designed NetEx, a bulk transfer system that opportunistically exploits the excess capacities of network links to deliver bulk content cheaply and efficiently. Our results based on data from both a commercial tier-1 ISP and the Abilene network suggest that NetEx can considerably increase the capacity of the network, and at the same time it can provide good average performance to bulk transfers.

Advances in technology enabled new types of networks to appear (e.g. PDA based spontaneous networks). Here, execution of transactions manipulating distributed objects is affected by the intermittent connectivity thereby causing unnecessary aborts. This paper presents a solution to make transactions resilient to intermittent connections thus increasing transaction throughput. This is achieved by i) allowing transactions to further span in time and/or ii) relaxing the consistency properties of transactions. For this purpose, application programmers specify the minimum transaction requirements (which depend on the application semantics) using policies. Evaluation shows that slightly increasing the maximum transaction execution time and/or reducing consistency, transaction throughput increases substantially. This solution is implemented in MobileTrans-a distributed object-oriented middleware system providing adaptive transactions aiding the reliable management of distributed object graphs. Policies are specifically designed to overcome the connectivity intermittence problem. The minimum transaction requirements are specified as parameters to these policies without having to change application code.