Photo

Contact details

Email:

maffeis at doc ic ac uk

Office:

Tel: +44 (0)2075948390
Room 441 Huxley Bldg.

Work Address:

Dr. Sergio Maffeis
Research Fellow
Department of Computing,
Imperial College London,
SW7 2AZ United Kingdom.
 

News

Now Hiring! Postdoc position available on Certified Verification of Client-Side Web Programs.
Click here for details.

Opportunities

Research

Curriculum Vitae

An up to date CV is available here.

Selected Publications

Below is a list of selected publications, divided by topic. A full (probably out of date) list is available here [PDF].


Towards a program logic for JavaScript.
P. Gardner, S. Maffeis, G. D. Smith. Proc. of POPL '12.
[PDF] Abstract. BibTeX.

Abstract: JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts. We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and "with". We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.
@inproceedings{DBLP:conf/popl/GardnerMS12,
  author    = {Philippa Gardner and
               Sergio Maffeis and
               Gareth David Smith},
  title     = {Towards a program logic for JavaScript},
  booktitle = {POPL},
  year      = {2012},
  pages     = {31-44},
}

Object Capabilities and Isolation of Untrusted Web Applications.
S. Maffeis, J.C. Mitchell and A. Taly. Proc. of IEEE Security & Privacy '10.
[PDF] Abstract. BibTeX.

Abstract: When a web site combines active content (applications) from untrusted sources, it is important to protect each untrusted application from the others. The object-capability model provides an appealing approach: if separate applications are provided disjoint capabilities, a sound object-capability framework should prevent untrusted applications from interfering with each other. However, in developing language-based foundations for isolation proofs based on object-capabilities, we identify a more general notion of authority safety that also implies resource isolation. After proving that capability safety implies authority safety, we consider three example languages and show the applicability of our framework. Perhaps surprisingly, although we prove that one JavaScript subset based on Google Caja is capability safe, a more expressive subset of JavaScript is actually authority safe and therefore suitable for isolating untrusted applications.
@inproceedings{mmt-oakland10,
    author= {S. Maffeis and J.C. Mitchell and A. Taly},
    title = {Object Capabilities and Isolation of Untrusted Web Applications},
    booktitle = "Proc of {IEEE Security and Privacy}'10",
    publisher = "IEEE",
    year = "2010"
}

Isolating JavaScript with Filters, Rewriting, and Wrappers.
S. Maffeis, J.C. Mitchell and A. Taly. Proc. of ESORICS'09.
[PDF] Abstract. BibTeX.

Abstract: We study methods that allow web sites to safely combine JavaSCript from untrusted sources. If implemented properly, filters can prevent dangerous code from loading into the execution environment, while rewriting allows greater expressiveness by inserting run-time checks. Wrapping properties of the execution environment can prevent misuse without requiring changes to imported JavaSCript. Using a formal semantics for the ECMA 262-3 standard language, we prove security properties of a subset of JavaScript, comparable in expressiveness to Facebook FBJS, obtained by combining three isolation mechanisms. The isolation guarantees of the three mechanisms are interdependent, with rewriting and wrapper functions relying on the absence of JavaScript constructs eliminated by language filters.
@inproceedings{mmt-esorics09,
    author= {S. Maffeis and J.C. Mitchell and A. Taly},
    title = {Isolating JavaScript with Filters, Rewriting, and Wrappers},
    booktitle = "Proc of {ESORICS}'09",
    publisher = "LNCS",
    year = "2009"
}

Run-Time Enforcement of Secure JavaScript Subsets.
S. Maffeis, J.C. Mitchell and A. Taly. Proc. of W2SP'09.
[PDF] Abstract. BibTeX.

Abstract: Many Web-based applications such as advertisement, social networking and online shopping benefit from the interaction of trusted and unstrusted content within the same page. If the untrusted content includes JavaScript code, it must be prevented from maliciously altering pages, stealing sensitive information, or causing other harm. We study filtering and rewriting techniques to control untrusted JavaScript code, using Facebook FBJS as a motivating example. We explain the core problems, provide JavaSCript code that enforces provable isolation properties at run-time, and compare our results with the techniques used in FBJS.
@inproceedings{mmt-w2sp09,
    author= {S. Maffeis and J.C. Mitchell and A. Taly},
    title = {Run-Time Enforcement of Secure JavaScript Subsets},
    booktitle = "Proc of {W2SP}'09",
    publisher = "IEEE",
    year = "2009"
}

Language-Based Isolation of Untrusted JavaScript.
S.Maffeis, J.C. Mitchell and A.Taly. Proc. of CSF'09.
[PDF] Abstract. BibTeX.

Abstract: Web sites that incorporate untrusted content may use browser- or language-based methods to keep such content from maliciously altering pages, stealing sensitive information, or causing other harm. We study methods for filtering and rewriting Javascript code, using Yahoo! AdSafe and Facebook FBJS as motivating examples. We explain the core problems by describing previously unknown vulnerabilities and shortcomings, and give a foundation for improved solutions based on an operational semantics of the full ECMA-262 language. We also discuss how to apply our analysis to address the problems we discovered.
@InProceedings{MMT-CSF-TR09,
  author       = "S. Maffeis and A. Taly",
  title        = "Language-based Isolation of Untrusted {J}avascript",
  booktitle    = "Proc. of {CSF}'09",
  series       = "IEEE",
  year         = "2009",
  note        = "{S}ee also: Dep. of Computing, Imperial College London, Technical Report DTR09-3, 2009.",
}

An Operational Semantics for Javascript.
S. Maffeis, J.C. Mitchell and A. Taly. Proc. of APLAS'08.
[PDF] Abstract. BibTeX.

Abstract: We define a small-step operational semantics for the ECMAScript standard language corresponding to JavaScript, as a basis for analyzing security properties of web applications and mashups. The semantics is based on the language standard and a number of experiments with different implementations and browsers. Some basic properties of the semantics are proved, including a soundness theorem and a characterization of the reachable portion of the heap.
@InProceedings{MMT-APLAS-TR08,
  author       = "S. Maffeis and J.C. Mitchell and A. Taly",
  title        = "An Operational Semantics for {JavaScript}",
  booktitle    = "Proc. of {APLAS}'08",
  series       = "LNCS",
  volume       = "5356",
  pages        = "307--325",
  year         = "2008",
  note        = "{S}ee also: Dep. of Computing, Imperial College London, Technical Report DTR08-13, 2008.",
}

Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage.
C. Bansal, K. Bhargavan, A. Delignat-Lavaud and S.Maffeis. Proc of POST'13
[PDF] Abstract. BibTeX.

Abstract: To protect sensitive user data against server-side attacks, a number of security-conscious web applications have turned to client-side encryption, where only encrypted user data is ever stored in the cloud. We formally investigate the security of a number of such applications, including password managers, cloud storage providers, an e-voting website and a conference management system. We show that their security relies on both their use of cryptography and the way it combines with common web security mechanisms as implemented in the browser. We model these applications using the WebSpi web security library for ProVerif, we discuss novel attacks found by automated formal analysis, and we propose robust countermeasures.
@MISC{bbdm:post13,
  author       = {Chetan Bansal and
                 Karthikeyan Bhargavan and
                 Antoine Delignat-Lavaud and
                 Sergio Maffeis},
  title        = {Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage},
  howpublished = {To appear in Proc. of POST'13},
  year         = {2013},
}

Discovering Concrete Attacks on Website Authorization by Formal Analysis.
C. Bansal, K. Bhargavan and S.Maffeis. Proc of CSF'12
[PDF] Abstract. BibTeX.

Abstract: Social sign-on and social sharing are becoming an ever more popular feature of web applications. This success is largely due to the APIs and support offered by prominent social networks, such as Facebook, Twitter, and Google, on the basis of new open standards such as the OAuth 2.0 authorization protocol. A formal analysis of these protocols must account for malicious websites and common web application vulnerabilities, such as cross-site request forgery and open redirectors. We model several configurations of the OAuth 2.0 protocol in the applied pi-calculus and verify them using ProVerif. Our models rely on WebSpi, a new library for modeling web applications and web-based attackers that is designed to help discover concrete website attacks. Our approach is validated by finding dozens of previously unknown vulnerabilities in popular websites such as Yahoo and WordPress, when they connect to social networks such as Twitter and Facebook.
@inproceedings{DBLP:conf/csfw/BansalBM12,
  author    = {Chetan Bansal and
               Karthikeyan Bhargavan and
               Sergio Maffeis},
  title     = {Discovering Concrete Attacks on Website Authorization by
               Formal Analysis},
  booktitle = {CSF},
  year      = {2012},
  pages     = {247-262},
}

Refinement Types for Secure Implementations.
J.Bengtson, K.Bhargavan, C.Fournet, A.Gordon and S.Maffeis. Transactions On Programming Languages And Systems, 2011.
[PDF] Abstract. BibTeX.

Abstract: 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 l-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.
@article{DBLP:journals/toplas/BengtsonBFGM11,
  author    = {Jesper Bengtson and
               Karthikeyan Bhargavan and
               C{\'e}dric Fournet and
               Andrew D. Gordon and
               Sergio Maffeis},
  title     = {Refinement types for secure implementations},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {33},
  number    = {2},
  year      = {2011},
  pages     = {8},
}

Code Carrying Authorization.
S.Maffeis, M.Abadi, C.Fournet and A.Gordon. Proc. of ESORICS'08.
[PDF] Abstract. BibTeX.

Abstract: In authorization, there is often a wish to shift the burden of proof to those making requests, since they may have more resources and more specific knowledge to construct the required proofs. We introduce an extreme instance of this approach, which we call Code-Carrying Authorization (CCA). With CCA, access-control decisions can partly be delegated to untrusted code obtained at run-time. The dynamic verification of this code ensures the safety of authorization decisions. We define and study this approach in the setting of a higher-order spi calculus. The type system of this calculus provides the needed support for static and dynamic verification.
@MISC{maff:aba:four:gor:esorics08,
  author =       {S. Maffeis and M. Abadi and C. Fournet and A. Gordon},
  title =        {Code Carrying Authorization},
  howpublished = {Proc. of Esorics'08},
  year =         {2008},
}

A Type Discipline for Authorization in Distributed Systems.
C.Fournet, A.Gordon and S.Maffeis. Proc. of CSF'07.
[PDF] Abstract. BibTeX.

Abstract: 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.
@MISC{Maffeis:aiamb:thesis00,
  author =       {C{\'e}dric Fournet and Andrew D. Gordon and Sergio Maffeis},
  title =        {A Type Discipline for Authorization in Distributed Systems},
  howpublished = {Proc. of CSF'07},
  year =         {2007},
}

A Type Discipline for Authorization Policies.
C.Fournet, A.Gordon and S.Maffeis. Transactions On Programming Languages And Systems, 2007.
[PDF] Abstract. BibTeX.

Abstract: 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, for instance, 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.
 @misc{FournetGordonMaffeis:toplas05,
  author    = {C. Fournet and
               A. D. Gordon and
               S. Maffeis},
  title     = {A Type Discipline for Authorization Policies},
  howpublished = {\emph{ACM TOPLAS}},
  year      = {2007},
}

On Abstract Interpretation of Mobile Ambients.
F.Levi and S.Maffeis. Information and Computation, 2004.
[PDF] Abstract. BibTeX.

Abstract: We introduce an abstract interpretation framework for Mobile Ambients, based on a new semantics called 'normal semantics'. Then, we derive within this setting two analyses computing a safe approximation of the run-time topological structure of processes. Such a static information can be successfully used to establish interesting security properties.
 @article{LeviMaffeis:aiamb:ic04,
  author = "Francesca Levi and Sergio Maffeis",
    title = "On Abstract Interpretation of Mobile Ambients",
    journal = "Information and Computation",
    volume = "188",
    issue = "2",
    pages = "179--240",
    month = "January",
    year = "2004",
}

Behavioural Equivalences for Dynamic Web Data.
S.Maffeis and P. Gardner. Journal of Logic and Algebraic Programming, 2008.
[PDF] Abstract. BibTeX.

Abstract: Peer-to-peer systems, exchanging dynamic documents through Web services, are a simple and effective platform for data integration on the internet. Dynamic documents can contain both data and references to external sources in the form of links, calls to web services, or coordination scripts. XML standards, and industrial platforms for web services, provide the technological basis for building such systems, and process algebras are a promising tool for studying and understanding their formal properties. Core Xdpi is the explicitly located version of Xdpi, a process calculus designed for reasoning about dynamic Web data, based on explicit repositories of higher-order semistructured data and pi-calculus-like processes which can communicate with each other, query and update the local repository, or migrate to other peers to continue execution. We study behavioural equivalences for Core Xdpi processes. To help with the proofs, which require a costly property of closure under contexts, we define a coinductive relation (called domain bisimilarity) which does not quantify over contexts and which entails process equivalence. Its definition is non-standard, because scripts are part of the values, and process equivalences are sensitive to the set of locations constituting the network. We apply our process equivalence to study some communication patterns used by servers in distributed query systems, and we propose a new pattern involving mobile code.
@MISC{MaffeisGardner:xdpi:JLAP05,
  author =       "S. Maffeis and P. Gardner",
  title =        "Behavioural Equivalences for Dynamic {W}eb Data",
  howpublished = "To appear in Elsevier JLAP",
  month =        feb,
  year =         "2008",
}

Dynamic Web Data: A Process Algebraic Approach.
S.Maffeis. Ph.D. Thesis, Imperial College London, 2006.
[PDF] Abstract. BibTeX.

Abstract: Peer to peer systems, exchanging dynamic documents through Web services, are a simple and effective platform for data integration on the internet. Dynamic documents can contain both data and references to external sources in the form of links, calls to web services, or coordination scripts. XML standards, and industrial platforms for web services, provide the technological basis for building such systems. We argue that process algebras are a promising tool for studying and understanding their formal properties. In this thesis, we define the Xdpi-calculus with the aim of reasoning about dynamic Web data. Xdpi terms represent networks of peers, each consisting of an XML data repository and a working space where processes are allowed to run. Processes, inspired by the pi-calculus, can communicate with each other, query and update the local repository, or migrate to other peers to continue execution. Data can contain scripted processes, which can be executed by other processes. For example, Xdpi processes can be used to embed service calls in documents and to model Web services. We investigate behavioural equivalences for Xdpi, comparing several observable properties, such as the shape of data trees and the communication actions attempted by processes. To simplify reasoning on equivalences, we introduce Core Xdpi, a calculus which is semantically equivalent to Xdpi, but where processes are located explicitly and are separated from the data repository. To help proving equivalences, which require a costly property of closure under contexts, we define a coinductive relation (called domain bisimilarity) which does not quantify over contexts and which entails process equivalence. Its definition is non-standard, because scripts are part of the values, and process equivalences are sensitive to the set of locations constituting the network. We apply bisimilarity to study some communication patterns used by servers in distributed query systems, and we propose a new pattern involving mobile code.
@PHDTHESIS{Maffeis:xdpi:phd05,
  AUTHOR =       {Sergio Maffeis},
  TITLE =        {Dynamic Web Data: A Process Algebraic Approach},
  SCHOOL =       {Imperial College London},
  month =        {August},
  YEAR =         {2006},
}

Modelling Dynamic Web Data.
P.Gardner and S.Maffeis. Theoretical Computer Science, 2005.
[PDF] Abstract. BibTeX.

Abstract: We introduce the Xdpi calculus, a peer-to-peer model for reasoning about dynamic web data. Web data is not just stored statically. Rather it is referenced indirectly, for example using hyperlinks, service calls, or scripts for dynamically accessing data, which require the complex coordination of data and processes between sites. The Xdpi calculus models this coordination, by integrating the XML data structure with process orchestration techniques associated with the distributed pi-calculus. We study behavioural equivalences for Xdpi, to analyze the various possible patterns of data and process interaction.
@ARTICLE{GardnerMaffeis:xdpi:tcs04,
  author =       {Philippa Gardner and Sergio Maffeis},
  title =        {Modelling Dynamic {Web} Data},
  journal = {Theoretical Computer Science},
  volume = {342},
  year =         {2005},
  pages  = {104--131},
}

Matching Systems for Concurrent Calculi.
B. Haagensen, S.Maffeis and I.Phillips. Proc. of Express'07.
[PDF] Abstract. BibTeX.

Abstract: 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.
@article{MaffeisPhillips:ambex:tcs04,
    author = "Bjorn Haagensen and Sergio Maffeis and Iain Phillips",
    title = "Matching Systems for Concurrent Calculi",
    journal = "Express'07",
    year = "2007",
}

On the Computational Strength of Pure Ambient Calculi.
S.Maffeis and I.Phillips. Theoretical Computer Science, 2005.
[PDF] Abstract. BibTeX.

Abstract: Cardelli and Gordon's calculus of Mobile Ambients has attracted widespread interest as a model of mobile computation. The standard calculus is quite rich, with a variety of operators, together with capabilities for entering, leaving and dissolving ambients. The question arises of what is a minimal Turing-complete set of constructs. Previous work has established that Turing completeness can be achieved without using communication or restriction. We show that it can be achieved merely using movement capabilities (and not dissolution). We also show that certain smaller sets of constructs are either terminating or have decidable termination.
@article{MaffeisPhillips:ambex:tcs04,
    author = "Sergio Maffeis and Iain Phillips",
    title = "On the Computational Strength of Pure Ambient Calculi",
    journal = "Theoretical Computer Science",
    year = "2005",
}

Sequence Types for the Pi-Calculus.
S.Maffeis. Proc. of ITRS'04.
[PDF] Abstract. BibTeX.

Abstract: We introduce 'channel sequence types' to study finitary polymorphism in the context of mobile processes modelled in the pi-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 pi-calculus with the strict intersection type discipline.
 @InProceedings{Maffeis:pi:itrs04,
  author =       "Sergio Maffeis",
  title =        "Sequence Types for the Pi-Calculus",
  booktitle =    "{ITRS}'04",
  year =         "2005",
  pages =        "117--132",
  volume =       "136",
  series =       "ENTCS",
  publisher =    Elsevier,
}

On the Expressive Power of Polyadic Synchronisation in Pi-Calculus.
M.Carbone and S.Maffeis. Nordic Journal of Computing, 2003.
[PDF] Abstract. BibTeX.

Abstract: We extend the pi-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 pi-calculus, we suggest that it permits divergence-free encodings of distributed calculi, and we show that a limited form of polyadic synchronisation can be encoded weakly in pi-calculus. After showing that matching cannot be derived in pi-calculus, we compare the expressivity of polyadic synchronisation, mixed choice and matching. In particular we show that the degree of synchronisation of a language increases its expressive power by means of a separation result in the style of Palamidessi's result for mixed choice.
@article{CarboneMaffeis:epi:njc03,
    author = "Marco Carbone and Sergio Maffeis",
    title = "On the Expressive Power of Polyadic Synchronisation in $\pi$-Calculus",
    journal = "Nordic Journal of Computing",
    volume = "10",
    number = "2",
    pages = "70--98",
    year = "2003",
}

Academic year 2013-2014

PROGRAMMING II - CO120

Aims of the course: The aims of this module are: To give students a good understanding of basic concepts of object-oriented program design; introduce them to the fundamental principles of abstraction, modularity and reusability; and illustrate object diagrams as a basic object-oriented design and modelling technique.
  • To teach and enable students to develop object-oriented programming skills within the Java language; to enable students to develop object-oriented Java program solutions to small application problems.
  • To help students gain a good understanding of, and ability to use, abstract data types; familiarise students with common abstract data types and associated operations.
  • To teach various design and implementation solutions for abstract data types; illustrate the practical effects of the different implementation choices; and illustrate their practical use in developing Java programs for real application problems.
For more details, see the course webpage.

Academic Writing for Computer Science - C520

I will run one of the Abstract Writing Exercise modules of the course. The aim is to summarise technical material in a clear and compelling way. For more details, see the course webpage.

Future Teaching

Network and Web Security
In the Academic year 2014-2015 I will theach the Web Security half of this course, part of the forthcoming Master in Secure Software Systems and also offered as a 3rd year undergraduate course.

Past Teaching