Authors: Focardi, Riccardo
Article Type: Editorial
DOI: 10.3233/JCS-2009-0390
Citation: Journal of Computer Security, vol. 18, no. 6, pp. 969-969, 2010
Authors: Focardi, Riccardo
Article Type: Editorial
DOI: 10.3233/JCS-2006-14201
Citation: Journal of Computer Security, vol. 14, no. 2, pp. 111-111, 2006
Authors: Focardi, Riccardo
Article Type: Editorial
DOI: 10.3233/JCS-2005-13301
Citation: Journal of Computer Security, vol. 13, no. 3, pp. 345-345, 2005
Authors: Focardi, Riccardo | Gorrieri, Roberto
Article Type: Research Article
Abstract: Several information flow security definitions, proposed in the literature, are generalized and adapted to the model of labelled transition systems. This very general model has been widely used as a semantic domain for many process algebras, e.g. CCS. As a by-product, we provide a process algebra similar to CCS with a set of security notions, hence relating these two areas of concurrency research. A classification of these generalized security definitions is presented, taking into account also the additional property of input totality, which can influence this taxonomy. We also show that some of these security properties are composable w.r.t. the …operators of parallelism and action restriction. Show more
DOI: 10.3233/JCS-1994/1995-3103
Citation: Journal of Computer Security, vol. 3, no. 1, pp. 5-33, 1995
Authors: Focardi, Riccardo | Rossi, Sabina
Article Type: Research Article
Abstract: We study information flow security in the setting of mobile agents. We propose a sufficient condition to security named Persistent_BNDC. A process is Persistent_BNDC when every of its reachable states satisfies a basic Non-Interference property called BNDC. By imposing that security persists during process execution, one is guaranteed that every potential migration is performed in a stable, secure state. We define a suitable bisimulation-based equivalence relation among processes, that allows us to express the new property as a single equivalence check, thus avoiding the universal quantifications over all the reachable states (required by Persistent_BNDC) and over all the possible hostile …environments (implicit in the basic Non-Interference property BNDC). We prove that Persistent_BNDC is a sufficient condition to the security of mobile agents by (i) giving a sound and complete characterization of Persistent_BNDC in terms of dynamic contexts, i.e., execution contexts that can non-deterministically change at run-time, abstractly modelling arbitrary migrations; (ii) showing that Persistent_BNDC implies information flow security when agent mobility is explicitly expressed in the calculus. Show more
Keywords: Information flow, Non-Interference, process calculi, mobility, bisimulation
DOI: 10.3233/JCS-2006-14103
Citation: Journal of Computer Security, vol. 14, no. 1, pp. 65-110, 2006
Authors: Bugliesi, Michele | Focardi, Riccardo | Maffei, Matteo
Article Type: Research Article
Abstract: 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 independently 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. Show more
DOI: 10.3233/JCS-2007-15602
Citation: Journal of Computer Security, vol. 15, no. 6, pp. 563-617, 2007
Authors: Centenaro, Matteo | Focardi, Riccardo | Luccio, Flaminia L.
Article Type: Research Article
Abstract: PKCS#11, is a security API for cryptographic tokens. It is known to be vulnerable to attacks which can directly extract, as cleartext, the value of sensitive keys. In particular, the API does not impose any limitation on the different roles a key can assume, and it permits to perform conflicting operations such as asking the token to wrap a key with another one and then to decrypt it. Fixes proposed in the literature, or implemented in real devices, impose policies restricting key roles and token functionalities. In this paper we define a simple imperative programming language, suitable to code PKCS#11 …symmetric key management, and we develop a type-based analysis to prove that the secrecy of sensitive keys is preserved under a certain policy. We formally analyse existing fixes for PKCS#11 and we propose a new one, which is type-checkable and prevents conflicting roles by deriving different keys for different roles. We develop a prototype type-checker for a software token emulator written in C and we experiment on various working configurations. Show more
Keywords: Security APIs, PKCS#11, language-based security, type systems
DOI: 10.3233/JCS-130479
Citation: Journal of Computer Security, vol. 21, no. 6, pp. 971-1007, 2013
Authors: Bugliesi, Michele | Calzavara, Stefano | Focardi, Riccardo | Khan, Wilayat
Article Type: Research Article
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. Show more
Keywords: Browser security, session cookies, formal methods, noninterference
DOI: 10.3233/JCS-150529
Citation: Journal of Computer Security, vol. 23, no. 4, pp. 509-537, 2015
Authors: Bodei, Chiara | Ceragioli, Lorenzo | Degano, Pierpaolo | Focardi, Riccardo | Galletta, Letterio | Luccio, Flaminia | Tempesta, Mauro | Veronese, Lorenzo
Article Type: Research Article
Abstract: Firewalls are essential for managing and protecting computer networks. They permit specifying which packets are allowed to enter a network, and also how these packets are modified by IP address translation and port redirection. Configuring a firewall is notoriously hard, and one of the reasons is that it requires using low level, hard to interpret, configuration languages. Equally difficult are policy maintenance and refactoring, as well as porting a configuration from one firewall system to another. To address these issues we introduce a pipeline that assists system administrators in checking if: (i) the intended security policy is actually implemented by …a configuration; (ii) two configurations are equivalent; (iii) updates have the desired effect on the firewall behavior; (iv) there are useless or redundant rules; additionally, an administrator can (v) transcompile a configuration into an equivalent one in a different language; and (vi) maintain a configuration using a generic, declarative language that can be compiled into different target languages. The pipeline is based on IFCL , an intermediate firewall language equipped with a formal semantics, and it is implemented in an open source tool called FWS. In particular, the first stage decompiles real firewall configurations for iptables , ipfw , pf and (a subset of) Cisco IOS into IFCL . The second one transforms an IFCL configuration into a logical predicate and uses the Z3 solver to synthesize an abstract specification that succinctly represents the firewall behavior. System administrators can use FWS to analyze the firewall by posing SQL-like queries, and update the configuration to meet the desired security requirements. Finally, the last stage allows for maintaining a configuration by acting directly on its abstract specification and then compiling it to the chosen target language. Tests on real firewall configurations show that FWS can be fruitfully used in real-world scenarios. Show more
Keywords: Firewall configuration languages, Semantic-based tool, Configuration analysis, refactoring, maintaining, porting
DOI: 10.3233/JCS-200017
Citation: Journal of Computer Security, vol. 29, no. 1, pp. 77-134, 2021
