Abstract We present an empirical study on the ability of Large Language Models (LLMs) to understand code by detecting semantically equivalent and inequivalent programs, that is, whether they compute the same result given the same input or not. To probe this, we deliberately perturb the program text by introducing semantics-preserving code transformations, namely copy propagation and constant folding. Using a benchmark of 11 Python functions with both equivalent and non-equivalent variants, we evaluate seven state-of-the-art LLMs (including ChatGPT, Claude, Gemini, and Deep-Seek) under zero-shot prompting, with and without minimal context. Despite strong performance in code generation tasks, the models often fail in this deeper reasoning challenge, misclassifying 41% of equivalent cases without context and 29% with context. Although prompting can improve performance, it does not address the underlying limitations of the models. We argue that improving LLMs themselves, through targeted fine-tuning, contrastive learning on equivalent and nonequivalent implementations, or training on transformation-invariant code, will be necessary for robust semantic understanding. Meanwhile, practitioners can achieve better results by selecting stronger models, carefully engineering prom-pts, or writing code with tools that normalize low-level differences before inference.

Smart contracts have played a pivotal role in the evolution of blockchains and Decentralized Applications (DApps). As DApps continue to gain widespread adoption, multiple smart contract languages have been and are being made available to developers, each with its distinctive features, strengths, and weaknesses. In this paper, we examine the smart contract languages used in major blockchain platforms, with the goal of providing a comprehensive assessment of their main properties. Our analysis targets the programming languages rather than the underlying architecture: as a result, while we do consider the interplay between language design and blockchain model, our main focus remains on language-specific features such as usability, programming style, safety and security. To conduct our assessment, we propose an original benchmark which encompasses a wide, yet manageable, spectrum of key use cases that cut across all the smart contract languages under examination. • We give an abstract overview of smart contract platforms, discussing the impact of different design choices. • We illustrate by examples how different design choices give rise to different programming styles for smart contracts. • We consider 6 leading smart contract languages: Solidity (Ethereum), Rust (Solana), Aiken (Cardano), PyTeal (Algorand), Move (Aptos), SmartPy (Tezos). • We develop an open-source benchmark of use cases of smart contracts, implemented in all the languages in our selection. • Based on our benchmark, we evaluate smart contract languages focussing on their security, code readability, usability, and functionalities.

Since cookies act as the only proof of a user identity, web sessions are particularly vulnerable to session hijacking attacks, where the browser run by a given user sends requests associated to the identity of another user. When [Formula: see text] cookies are used to implement a session, there might actually be n sub-sessions running at the same website, where each cookie is used to retrieve part of the state information related to the session. Sub-session hijacking breaks the ideal view of the existence of a unique user session by selectively hijacking m sub-sessions, with [Formula: see text]. This may reduce the security of the session to the security of its weakest sub-session. In this paper, we take a systematic look at the root causes of sub-session hijacking attacks and we introduce sub-session linking as a possible defense mechanism. Out of two flavors of sub-session linking desirable for security, which we call intra-scope and inter-scope sub-session linking respectively, only the former is relatively smooth to implement. Luckily, we also identify programming practices to void the need for inter-scope sub-session linking. We finally present Warden, a server-side proxy which automatically enforces intra-scope sub-session linking on incoming HTTP(S) requests, and we evaluate it in terms of protection, performances, backward compatibility and ease of deployment.

Content Security Policy (CSP) is a recent W3C standard introduced to prevent and mitigate the impact of content injection vulnerabilities on websites. In this article, we introduce a formal semantics for the latest stable version of the standard, CSP Level 2. We then perform a systematic, large-scale analysis of the effectiveness of the current CSP deployment, using the formal semantics to substantiate our methodology and to assess the impact of the detected issues. We focus on four key aspects that affect the effectiveness of CSP: browser support, website adoption, correct configuration, and constant maintenance. Our analysis shows that browser support for CSP is largely satisfactory, with the exception of a few notable issues. However, there are several shortcomings relative to the other three aspects. CSP appears to have a rather limited deployment as yet and, more crucially, existing policies exhibit a number of weaknesses and misconfiguration errors. Moreover, content security policies are not regularly updated to ban insecure practices and remove unintended security violations. We argue that many of these problems can be fixed by better exploiting the monitoring facilities of CSP, while other issues deserve additional research, being more rooted into the CSP design.

Content Security Policy (CSP) is an emerging W3C standard introduced to mitigate the impact of content injection vulnerabilities on websites. We perform a systematic, large-scale analysis of four key aspects that impact on the effectiveness of CSP: browser support, website adoption, correct configuration and constant maintenance. While browser support is largely satisfactory, with the exception of few notable issues, our analysis unveils several shortcomings relative to the other three aspects. CSP appears to have a rather limited deployment as yet and, more crucially, existing policies exhibit a number of weaknesses and misconfiguration errors. Moreover, content security policies are not regularly updated to ban insecure practices and remove unintended security violations. We argue that many of these problems can be fixed by better exploiting the monitoring facilities of CSP, while other issues deserve additional research, being more rooted into the CSP design.

Presents the introductory welcome message from the conference proceedings. May include the conference officers' congratulations to all involved with the conference event and publication of the proceedings record.

Authorization in workflow systems is usually built on top of role-based access control (RBAC), security policies on workflows are then expressed as constraints on the users performing a set of tasks and the roles assigned to them. Unfortunately, when role administration is distributed and potentially untrusted users contribute to the role assignment process, like in the case of Administrative RBAC (ARBAC), collusions may take place to circumvent the intended workflow security policies. In a collusion attack, a set of users of a workflow system collaborates by changing the user-to-role assignment, so as to sidestep the security policies and run up to completion a workflow they could not complete otherwise. In this paper, we study the problem of collusion attacks in a formal model of workflows based on stable event structures and we define a precise notion of security against collusion. We then propose a static analysis technique based on a reduction to a role reachability problem for ARBAC, which can be used to prove or disprove security for a large class of workflow systems. We also discuss how to aggressively optimise the obtained role reachability problem to ensure its tractability. Finally, we implement our analysis in a tool, WARBAC, and we experimentally show its effectiveness on a set of publicly available examples, including a realistic case study.

Model-checking is a popular approach to the security analysis of ARBAC policies, but its effectiveness is hindered by the exponential explosion of the ways in which different users can be assigned to different role combinations. In this paper we propose a paradigm shift, based on the observation that, while verifying ARBAC by exhaustive state search is complex, realistic policies often have rather simple security proofs, and we propose to use types as an effective tool to leverage this simplicity. Concretely, we present a static type system to verify the security of ARBAC policies, along with a sound and complete type inference algorithm used to automate the verification process. We then introduce compositionality results, which identify sufficient conditions to preserve the security guarantees obtained by the verification of different sub-policies when these sub-policies are combined together: this compositional reasoning is crucial when policy administration is highly distributed and naturally supports the security analysis of evolving ARBAC policies. We evaluate our approach by implementing TAPA, a static analyser for ARBAC policies based on our theory, which we test on a number of relatively large, publicly available policies from the literature.

Abstract Session cookies constitute one of the main attack targets against client authentication on the Web. To counter these attacks, modern web browsers implement native cookie protection mechanisms based on the HttpOnly and Secure flags. While there is a general understanding about the effectiveness of these defenses, no formal result has so far been proved about the security guarantees they convey. With the present paper we provide the first such result, by presenting a mechanized proof of noninterference assessing the robustness of the HttpOnly and Secure cookie flags against both web and network attackers with the ability to perform arbitrary XSS code injection. We then develop CookiExt , a browser extension that provides client-side protection against session hijacking, based on appropriate flagging of session cookies and automatic redirection over HTTPS for HTTP requests carrying these cookies. Our solution improves over existing client-side defenses by combining protection against both web and network attacks, while at the same time being designed so as to minimise its effects on the user’s browsing experience. Finally, we report on the experiments we carried out to practically evaluate the effectiveness of our approach.

Recent research has shown that it is possible to leverage general-purpose theorem-proving techniques to develop powerful type systems for the verification of a wide range of security properties on application code. Although successful in many respects, these type systems fall short of capturing resource-conscious properties that are crucial in large classes of modern distributed applications. In this article, we propose the first type system that statically enforces the safety of cryptographic protocol implementations with respect to authorization policies expressed in affine logic. Our type system draws on a novel notion of “exponential serialization” of affine formulas, a general technique to protect affine formulas from the effect of duplication. This technique allows formulate of an expressive logical encoding of the authentication mechanisms underpinning distributed resource-aware authorization policies. We discuss the effectiveness of our approach on two case studies: the EPMO e-commerce protocol and the Kerberos authentication protocol. We finally devise a sound and complete type-checking algorithm, which is the key to achieving an efficient implementation of our analysis technique.

Browser-based defenses have recently been advocated as an effective mechanism to protect potentially insecure web applications against the threats of session hijacking, fixation, and related attacks. In existing approaches, all such defenses ultimately rely on client-side heuristics to automatically detect cookies containing session information, to then protect them against theft or otherwise unintended use. While clearly crucial to the effectiveness of the resulting defense mechanisms, these heuristics have not, as yet, undergone any rigorous assessment of their adequacy. In this article, we conduct the first such formal assessment, based on a ground truth of 2,464 cookies we collect from 215 popular websites of the Alexa ranking. To obtain the ground truth, we devise a semiautomatic procedure that draws on the novel notion of authentication token , which we introduce to capture multiple web authentication schemes. We test existing browser-based defenses in the literature against our ground truth, unveiling several pitfalls both in the heuristics adopted and in the methods used to assess them. We then propose a new detection method based on supervised learning , where our ground truth is used to train a set of binary classifiers, and report on experimental evidence that our method outperforms existing proposals. Interestingly, the resulting classifiers, together with our hands-on experience in the construction of the ground truth, provide new insight on how web authentication is actually implemented in practice.

Abstract—Enforcing protection at the browser side has recently become a popular approach for securing web authentication. Though interesting, existing attempts in the literature only address specific classes of attacks, and thus fall short of providing robust foundations to reason on web authentication security. In this paper we provide such foundations, by introducing a novel notion of web session integrity, which allows us to capture many existing attacks and spot some new ones. We then propose FF+, a security-enhanced model of a web browser that provides a full-fledged and provably sound enforcement of web session integrity. We leverage our theory to develop SESSINT, a prototype extension for Google Chrome implementing the security mechanisms formalized in FF+. SESSINT provides a level of security very close to FF+, while keeping an eye at usability and user experience. I.

Browser-based defenses have recently been advocated as an effective mechanism to protect web applications against the threats of session hijacking, fixation, and related attacks. In existing approaches, all such defenses ultimately rely on client-side heuristics to automatically detect cookies containing session information, to then protect them against theft or otherwise unintended use. While clearly crucial to the effectiveness of the resulting defense mechanisms, these heuristics have not, as yet, undergone any rigorous assessment of their adequacy. In this paper, we conduct the first such formal assessment, based on a gold set of cookies we collect from 70 popular websites of the Alexa ranking. To obtain the gold set, we devise a semi-automatic procedure that draws on a novel notion of authentication token, which we introduce to capture multiple web authentication schemes. We test existing browser-based defenses in the literature against our gold set, unveiling several pitfalls both in the heuristics adopted and in the methods used to assess them. We then propose a new detection method based on supervised learning, where our gold set is used to train a binary classifier, and report on experimental evidence that our method outperforms existing proposals. Interestingly, the resulting classification, together with our hands-on experience in the construction of the gold set, provides new insight on how web authentication is implemented in practice.

Role-based Access Control (RBAC) is one of the most widespread security mechanisms in use today. Given the growing complexity of policy languages and access control systems, verifying that such systems enforce the desired invariants is recognized as a security problem of crucial importance. In the present paper, we develop a framework for the formal verification of grsecurity, an access control system developed on top of Unix/Linux systems. The verification problem in grsecurity presents much of the complexity of modern RBAC systems, due to the presence of policy state changes that may arise both from explicit administrative primitives supported by grsecurity, and as the result of the interaction with the underlying operating system facilities. We develop a formal semantics for grsecurity's RBAC system, based on a labelled transition system, and a sound abstraction of that semantics providing a bounded approximation, amenable to model checking. We report on the result of the experimental analysis conducted with gran, the model checker we implemented based on our abstract semantics, on existing public servers running grsecurity to implement their RBAC systems.

Type systems for authorization are a popular device for the specification and verification of security properties in cryptographic applications. Though promising, existing frameworks exhibit limited expressive power, as the underlying specification languages fail to account for powerful notions of authorization based on access counts, usage bounds, and mechanisms of resource consumption, which instead characterize most of the modern online services and applications. We present a new type system that features a novel combination of affine logic, refinement types, and types for cryptography, to support the verification of resource-aware security policies. The type system allows us to analyze a number of cryptographic protocol patterns and security properties, which are out of reach for existing verification frameworks based on static analysis.

Process algebraic techniques for distributed systems are increasingly being targeted at identifying abstractions that are adequate for both high-level programming and specification and security analysis and verification. Drawing on our earlier work in Bugliesi and Focardi, (2008), we investigate the expressive power of a core set of security and network abstractions that provide high-level primitives for specifying the honest principals in a network, while at the same time enabling an analysis of the network-level adversarial attacks that may be mounted by an intruder. We analyse various bisimulation equivalences for security that arise from endowing the intruder with: (i) different adversarial capabilities; and (ii) increasingly powerful control over the interaction among the distributed principals of a network. By comparing the relative strength of the bisimulation equivalences, we obtain a direct measure of the intruder's discriminating power, and hence of the expressiveness of the corresponding intruder model.

Discretionary Access Control (DAC) systems provide powerful resource management mechanisms based on the selective distribution of capabilities to selected classes of principals. We study a type-based theory of DAC models for a process calculus that extends Cardelli, Ghelli and Gordon's pi-calculus with groups (Cardelliet al. 2005). In our theory, groups play the role of principals and form the unit of abstraction for our access control policies, and types allow the specification of fine-grained access control policies to govern the transmission of names, bound the (iterated) re-transmission of capabilities and predicate their use on the inability to pass them to third parties. The type system relies on subtyping to achieve a selective distribution of capabilities to the groups that control the communication channels. We show that the typing and subtyping relationships of the calculus are decidable. We also prove a type safety result, showing that in well-typed processes all names: (i) flow according to the access control policies specified by their types; and (ii) are received at the intended sites with the intended capabilities. We illustrate the expressive power and the flexibility of the typing system using several examples.

Secure communication in distributed systems is notoriously hard to achieve due to the variety of attacks an adversary can mount, based on message interception, modification, redirection, eavesdropping or, even more subtly, on traffic analysis. In the literature on process calculi, traditional solutions to the problem either draw on low-level cryptographic primitives, as in the spi or applied-pi calculi, or rely on very abstract, and hard-to-implement, mechanisms to hide communication by means of private channels, as in the pi-calculus. A more recent line of research follows a different approach, aimed at identifying security primitives adequate as high-level programming abstractions, and at the same time well-suited for security analysis and verification in adversarial settings. The present paper makes a step further in that direction. We develop a calculus of secure communication based on core abstractions that support concise, high-level programming idioms for distributed, security-sensitive applications, and at the same time are powerful enough to express a full-fledged adversarial setting. Drawing on this calculus, we investigate reasoning methods for security based on the long-established practice by which security properties are defined in terms of behavioral equivalences. We give a co-inductive characterization of behavioral equivalence, in terms of bisimulation, and develop powerful up-to techniques to provide simple co-inductive proofs. We illustrate the adequacy of the model with several security laws for secrecy and authentication.

The challenges hidden in the implementation of high-level process calculi into low-level environments are well understood [3]. This paper develops a secure implementation of a typed pi calculus, in which capability types are employed to realize the policies for the access to communication channels. Our implementation compiles high-level processes of the pi-calculus into low-level principals of a cryptographic process calculus based on the applied-pi calculus [1]. In this translation, the high-level type capabilities are implemented as term capabilities protected by encryption keys only known to the intended receivers. As such, the implementation is effective even when the compiled, low-level principals are deployed in open contexts for which no assumption on trust and behavior may be made. Our technique and results draw on, and extend, previous work on secure implementation of channel abstractions in a dialect of the join calculus [2]. In particular, our translation preserves the forward secrecy of communications in a calculus that includes matching and supports the dynamic exchange of write and read access-rights among processes. We establish the adequacy and full abstraction of the implementation by contrasting the untyped equivalences of the low-level cryptographic calculus, with the typed equivalences of the high-level source calculus.

We propose a type and effect system for authentication protocols built upon a tagging scheme that formalizes the intended semantics of ciphertexts. The main result is that the validation of each component in isolation is provably sound and fully compositional: if all the protocol participants are i ndependently validated, then the protocol as a whole guarantees authentication in the presence of Dolev–Yao intruders possibly sharing long term keys with honest principals. Protocols are thus validated in the presence of both malicious outsiders and compromised insiders. The highly compositional nature of the analysis makes it suitable for multi-protocol systems, where different protocols might be executed concurrently.

This paper contrasts two existing type-based techniques for the analysis of authentication protocols. The former, proposed by Gordon and Jeffrey, uses dependent types for nonces and cryptographic keys to statically regulate the way that nonces are created and checked in the authentication exchange. The latter, proposed by the authors, relies on a combination of static and dynamic typing to achieve similar goals. Specifically, the type system employs dependent ciphertext types to statically define certain tags that determine the typed structure of the messages circulated in the authentication exchange. The type tags are then checked dynamically to verify that each message has the format expected at the corresponding step of the authentication exchange. This paper compares the two approaches, drawing on a translation of tagged protocols, validated by our system, into protocols that type check with Gordon and Jeffrey's system. This translation gives new insight into the tradeoffs between the two techniques, and on their relative expressiveness and precision. In addition, it allows us to port verification techniques from one setting to the other.

Non-interference has been advocated by various authors as a uniform framework for the formal specification of security properties in cryptographic protocols. Unfortunately, specifications based on non-interference are often non-effective, as they req

Boxed Ambients are a variant of Mobile Ambients that result from dropping the open capability and introducing new primitives for ambient communication. The new model of communication is faithful to the principles of distribution and location-awareness of Mobile Ambients, and complements the constructs in and out for mobility with finer-grained mechanisms for ambient interaction. We introduce the new calculus, study the impact of the new mechanisms for communication of typing and mobility, and show that they yield an effective framework for resource protection and access control in distributed systems.

Finding typed encodings of object-oriented into procedural or functional programming sheds light on the theoretical foundations of object-oriented languages and their specific typing constructs and techniques. This article describes a type preserving and computationally adequate interpretation of a full-fledged object calculus that supports message passing and constructs for object update and extension. The target theory is a higher-order λ-calculus with records and recursive folds/unfolds, polymorphic and recursive types, and subtyping. The interpretation specializes to calculi of nonextensible objects, and validates the expected subtypin

Secure Safe Ambients (SSA) are a typed variant of Safe Ambients [9], whose type system allows behavioral invariants of ambients to be expressed and verified. The most significant aspect of the type system is its ability to capture both explicit and implicit process and ambient behavior: process types account not only for immediate behavior, but also for the behavior resulting from capabilities a process acquires during its evolution in a given context. Based on that, the type system provides for static detection of security attacks such as Trojan Horses and other combinations of malicious agents.We study the type system of SSA, define algorithms for type checking and type reconstruction, define powerful languages for expressing security properties, and study a distributed version of SSA and its type system. For the latter, we show that distributed type checking ensures security even in ill-typed contexts, and discuss how it relates to the security architecture of the Java Virtual Machine.

Several calculi of objects have been studied in the recent literature, that support the central features of object-based languages: messages, inheritance, dynamic dispatch, object update and object-extension. We show that a complete semantic account of these features may be given in a fragment of higher-order linear logic.

We extend the type system for the Lambda Calculus of Objects [16] with a mechanism of width subtyping and a treatment of incomplete objects. The main novelties over previous work are the use of subtype-bounded quantification to capture a new and more direct rendering of MyType polymorphism, and a uniform treatment for other features that were accounted for via different systems in subsequent extensions [7, 6] of [16]. The new system provides for (i) appropriate type specialization of inherited methods, (ii) static detection of errors, (iii) width subtyping compatible with object extension, and (iv) sound typing for partially specified objects.

In this paper we define a compositional semantics for a generalized composition operator on logic programs. Static and dynamic inheritance as well as composition by union of clauses can all be obtained by specializing the general operator. The semantics is based on the notion of differential programs, logic programs annotated with declarations that establish the programs' external interfaces.