Publications
60 results found
Maffeis S, Mitchell JC, Taly A, 2010, Object Capabilities and Isolation of Untrusted Web Applications, Symposium on Security and Privacy, Publisher: IEEE COMPUTER SOC, Pages: 125-140, ISSN: 1081-6011
- Author Web Link
- Cite
- Citations: 31
Maffeis S, Mitchell JC, Taly A, 2009, Isolating JavaScript with filters, rewriting, and wrappers, Departmental Technical Report: 09/6, Publisher: Department of Computing, Imperial College London, 09/6
We study methods that allow web sites to safely combine JavaScriptfrom untrusted sources. If implemented properly, lters can prevent dangerouscode from loading into the execution environment, while rewriting allows greaterexpressiveness by inserting run-time checks. Wrapping properties of the execu-tion environment can prevent misuse without requiring changes to importedJavaScript.Using a formal semantics for the ECMA 262-3 standard language, we provesecurity properties of a subset of JavaScript, comparable in expressiveness toFacebook FBJS, obtained by combining three isolation mechanisms. The isola-tion guarantees of the three mechanisms are interdependent, with rewriting andwrapper functions relying on the absence of JavaScript constructs eliminatedby language lters.
Maffeis S, Mitchell JC, Taly A, 2009, Language-based isolation of untrusted JavaScript, Departmental Technical Report: 09/3, Publisher: Department of Computing, Imperial College London, 09/3
Web sites that incorporate untrusted content may use browser- orlanguage-based methods to keep such content from maliciously altering pages,stealing sensitive information, or causing other harm. We study languagebasedmethods for ltering and rewriting JavaScript code, using Yahoo! ADSafeand Facebook FBJS as motivating examples. We explain the core problemsby describing previously unknown vulnerabilities and subtleties, anddevelop a foundation for improved solutions based on an operational semanticsof the full ECMA-262 language.We also discuss how to apply our analysisto address the JavaScript isolation problems we discovered.
Maffeis S, Mitchell JC, Taly A, 2009, Isolating JavaScript with Filters, Rewriting, and Wrappers, 14th European Symposium on Research in Computer Security (ESORICS 2009), Publisher: SPRINGER-VERLAG BERLIN, Pages: 505-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 24
Maffeis S, Taly A, 2009, Language-Based Isolation of Untrusted JavaScript, 22nd IEEE Computer Security Foundations Symposium, Publisher: IEEE COMPUTER SOC, Pages: 77-+
- Author Web Link
- Cite
- Citations: 23
Maffeis S, Gordon A, Fournet C, et al., 2008, Refinement Types for Secure Implementations, CSF '08, 21st IEEE Symposium on Computer Security Foundations 2008, Publisher: IEEE Computer Society, Pages: 17-32
We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a lambda-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.
Maffeis S, Gardner P, 2008, Behavioural equivalences for dynamic web data, JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, Vol: 75, Pages: 86-138, ISSN: 1567-8326
Maffeis S, Mitchell JC, Taly A, 2008, An operational semantics for JavaScript, Departmental Technical Report: 08/13, Publisher: Department of Computing, Imperial College London, 08/13
We de ne a small-step operational semantics for the ECMAScriptstandard language corresponding to JavaScript, as a basis for analyzing securityproperties of web applications and mashups. The semantics is based on thelanguage standard and a number of experiments with di erent implementationsand browsers. Some basic properties of the semantics are proved, including asoundness theorem and a characterization of the reachable portion of the heap.
Maffeis S, Mitchell JC, Taly A, 2008, An Operational Semantics for JavaScript, 6th Asian Symposium on Programming Languages and Systems, Publisher: SPRINGER-VERLAG BERLIN, Pages: 307-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 47
Haagensen B, Maffeis S, Phillips I, 2008, Matching systems for concurrent calculi, 14th International Workshop on Expressiveness in Concurrency (Express'07), Publisher: Elsevier, Pages: 85-99
Matching systems were introduced by Carbone and Maffeis, and used to investigate the expressiveness of the pi-calculus with polyadic synchronisation. We adapt their definition and investigate matching systems for CCS, the pi-calculus and Mobile Ambients. We show among other results that the asynchronous pi-calculus with matching cannot be encoded (under certain conditions) in CCS with polyadic synchronisation of all finite levels.
Maffeis S, Abadi M, Fournet C, et al., 2008, Code-Carrying Authorization, 13th European Symposium on Research in Computer Security, Publisher: SPRINGER-VERLAG BERLIN, Pages: 563-+, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 10
Fournet C, Gordon AD, Maffeis S, 2007, A type discipline for authorization in distributed systems, Pages: 31-45, ISSN: 1940-1434
We consider the problem of statically verifying the conformance of the code of a system to an explicit authorization policy. In a distributed setting, some part of the system may be compromised, that is, some nodes of the system and their security credentials may be under the control of an attacker. To help predict and bound the impact of such partial compromise, we advocate logic-based policies that explicitly record dependencies between principals. We propose a conformance criterion, safety despite compromised principals, such that an invalid authorization decision at an uncompromised node can arise only when nodes on which the decision logically depends are compromised. We formalize this criterion in the setting of a process calculus, and present a verification technique based on a type system. Hence, we can verify policy conformance of code that uses a wide range of the security mechanisms found in distributed systems, ranging from secure channels down to cryptographic primitives, including encryption and public-key signatures. © 2007 IEEE.
Fournet C, Gordon AD, Maffeis S, 2007, A type discipline for authorization policies, ACM Transactions on Programming Languages and Systems, Vol: 29, Pages: 25-25, ISSN: 0164-0925
<jats:p>Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs in particular can express policies in a simple, abstract manner.</jats:p> <jats:p>We consider the problem of checking whether a distributed implementation based on communication channels and cryptography complies with a logical authorization policy. We formalize authorization policies and their connection to code by embedding logical predicates and claims within a process calculus. We formulate policy compliance operationally by composing a process model of the distributed system with an arbitrary opponent process. Moreover, we propose a dependent type system for verifying policy compliance of implementation code. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.</jats:p>
Fournet C, Gordon AD, Maffeis S, 2007, A type discipline for authorization policies - art. no. 25, 14th European Symposium on Programming (ESOP 2005), Pages: 25-25
Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs in particular can express policies in a simple, abstract manner.We consider the problem of checking whether a distributed implementation based on communication channels and cryptography complies with a logical authorization policy. We formalize authorization policies and their connection to code by embedding logical predicates and claims within a process calculus. We formulate policy compliance operationally by composing a process model of the distributed system with an arbitrary opponent process. Moreover, we propose a dependent type system for verifying policy compliance of implementation code. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.
Maffeis S, 2007, Dynamic Web Data and Process Calculi., Bull. EATCS, Vol: 93, Pages: 76-97
Maffeis S, 2006, Process Calculi and Peer-to-peer Web Data Integration, Pages: 233-236, ISSN: 1571-0661
Peer-to-peer systems exchanging dynamic documents through web services are a simple and effective platform for data integration on the Web. Dynamic documents can contain both data and declarative references to external sources, in the form of links, service calls, or coordination scripts. XML standards and industrial platforms for web services provide a wide technological basis for building such systems. We argue that process algebras are a promising tool for studying and understanding their formal properties. © 2006 Elsevier B.V. All rights reserved.
Gardner P, Maffeis S, 2005, Modelling dynamic web data, Theoretical Computer Science, Vol: 342, Pages: 104-131, ISSN: 0304-3975
Maffeis S, 2005, Sequence types for the π-calculus, Pages: 117-132, ISSN: 1571-0661
We introduce channel sequence types to study finitary polymorphism in the context of mobile processes modelled in the π-calculus. We associate to each channel a set of exchange types, and we require that output processes send values of one of those types, and input processes accept values of any type in the set. Our type assignment system enjoys subject reduction and guarantees the absence of communication errors. We give several examples of polymorphism, and we encode the λ-calculus with the strict intersection type discipline. © 2005 Elsevier B.V. All rights reserved.
Maffeis S, Phillips L, 2005, On the computational strength of pure ambient calculi, 10th International Workshop on Expressiveness in Concurrency (EXPRESS 2003), Publisher: ELSEVIER, Pages: 501-551, ISSN: 0304-3975
- Author Web Link
- Cite
- Citations: 21
Fournet C, Gordon AD, Maffeis S, 2005, A type discipline for authorization policies, 14th European Symposium on Programming (ESOP 2005), Publisher: SPRINGER-VERLAG BERLIN, Pages: 141-156, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 26
Levi F, Maffeis S, 2004, On abstract interpretation of mobile ambients, INFORMATION AND COMPUTATION, Vol: 188, Pages: 179-240, ISSN: 0890-5401
- Author Web Link
- Cite
- Citations: 11
Maffeis S, Phillips I, 2004, On the computational strength of pure ambient calculi, Pages: 29-49, ISSN: 1571-0661
Maffeis S, Gardner P, 2004, Behavioural equivalences for dynamic web data, Dordrecht, IFIP WCC-TCS'04 3rd international conference on theoretical computer science held at the 18th world computer congress, Toulouse, France, 22 - 27 August 2004, Publisher: Springer, Pages: 535-548
Gardner P, Maffeis S, 2004, Modelling dynamic web data, Berlin, 9th international workshop on data bases and programming languages Potsdam, Germany, 2003, Publisher: Springer-Verlag, Pages: 130-146
Gardner P, Maffeis S, 2003, Modelling dynamic web data, Departmental Technical Report: 03/14, Publisher: Department of Computing, Imperial College London, 03/14
We introduce Xd¼, a peer-to-peer model for reasoning about the dynamicbehaviour of web data. It is based on an idealised model of semistructureddata, and an extension of the ¼-calculus with process mobilityand with operations for interacting with data. Our model can be usedto reason about behaviour found in, for example, dynamic web page programming,applet interaction, and service orchestration. We study behaviouralequivalences for Xd¼, motivated by examples.
Maffeis S, 2003, On the computational strength of pure ambient calculi, Departmental Technical Report: 03/10, Publisher: Department of Computing, Imperial College London, 03/10
Cardelli and Gordon's calculus of Mobile Ambients has attracted widespread interestas a model of mobile computation. The standard calculus is quite rich, with a varietyof operators, together with capabilities for entering, leaving and dissolving ambi-ents. The question arises of what is a minimal Turing-complete set of constructs.Previous work has established that Turing completeness can be achieved withoutusing communication or restriction. We show that it can be achieved merely usingmovement capabilities (and not dissolution). We also show that certain smaller setsof constructs are either terminating or have decidable termination.
Carbone M, Maffeis S, 2003, On the Expressive Power of Polyadic Synchronisation in pi-calculus, Nordic Journal of Computing, Vol: 10, Pages: 70-98
Carbone M, Maffeis S, 2003, On the expressive power of polyadic synchronisation in Pi-calculus, 9th international workshop on expressiveness in concurrency, Express 02, Brno, Czech Republic, Publisher: Publishing Association, Pages: 70-98
Carbone M, Maffeis S, 2002, On the expressive power of polyadic synchronisation in π-calculus, Pages: 15-32, ISSN: 1571-0661
We extend the π-calculus with polyadic synchronisation, a generalisation of the communication mechanism which allows channel names to be composite. We show that this operator embeds nicely in the theory of π-calculus, and makes it possible to derive divergence-free encodings of distributed calculi. We give a separation result between the π-calculus with polyadic synchronisation (eπ) and the original calculus, in the style of an analogous result given by Palamidessi for mixed choice. We encode Local Area π showing how to control the local use of resources in eπ. Acknowledgments. We would like to thank Frank Valencia, Maria Vigliotti, Mogens Nielsen and Andrew Phillips for many useful comments and discussions. We are much indebted to the anonymous referees for the many suggestions that have allowed us to improve the final version of this paper. © 2002 Published by Elsevier Science B.V.
Levi F, Maffeis S, 2001, An abstract interpretation framework for analysing mobile ambients, Pages: 395-411, ISSN: 0302-9743
We introduce an abstract interpretation framework for Mobile Ambients, based on a new fixed-point semantics. Then, we derive within this setting two analyses computing a safe approximation of a property about the run-time topological structure of processes which is relevant to security. © Springer-Verlag Berlin Heidelberg 2001.
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.