Imperial College London

DrSergioMaffeis

Faculty of EngineeringDepartment of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8390sergio.maffeis Website

 
 
//

Location

 

441Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

39 results found

Arceri V, Maffeis S, 2017, Abstract Domains for Type Juggling, Publisher: ELSEVIER SCIENCE BV, Pages: 41-55, ISSN: 1571-0661

CONFERENCE PAPER

Bella G, Maffeis S, 2016, Special track on computer security (SEC), Pages: 2031-2032

CONFERENCE PAPER

Bella G, Maffeis S, 2015, 2015 Special Track on Computer Security, Pages: 2125-2126

CONFERENCE PAPER

Hothersall-Thomas C, Maffeis S, Novakovic C, 2015, BrowserAudit: Automated testing of browser security features, Pages: 37-47

The security of the client side of a web application relies on browser features such as cookies, the same-origin policy and HTTPS. As the client side grows increasingly powerful and sophisticated, browser vendors have stepped up their offering of security mechanisms which can be leveraged to protect it. These are often introduced experimentally and informally and, as adoption increases, gradually become standardised (e.g., CSP, CORS and HSTS). Considering the diverse landscape of browser vendors, releases, and customised versions for mobile and embedded devices, there is a compelling need for a systematic assessment of browser security. We present BrowserAudit, a tool for testing that a deployed browser enforces the guarantees implied by the main standardised and experimental security mechanisms. It includes more than 400 fully-automated tests that exercise a broad range of security features, helping web users, application developers and security researchers to make an informed security assessment of a deployed browser. We validate BrowserAudit by discovering both fresh and known security-related bugs in major browsers. Copyright is held by the owner/author(s).

CONFERENCE PAPER

Bansal C, Bhargavan K, Delignat-Lavaud A, Maffeis Set al., 2014, Discovering concrete attacks on website authorization by formal analysis, Journal of Computer Security, Vol: 22, Pages: 601-657, ISSN: 0926-227X

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 attacks on websites. To ease the task of writing formal models in our framework, we present a model extraction tool that automatically translates programs written in subsets of PHP and JavaScript to the applied pi-calculus. 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. © 2014-IOS Press.

JOURNAL ARTICLE

Bhargavan K, Delignat-Lavaud A, Maffeis S, 2014, Defensive javascript building and verifying secure web components, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 8604, Pages: 88-123, ISSN: 0302-9743

© Springer International Publishing Switzerland 2014. Defensive JavaScript (DJS) is a typed subset of JavaScript that guarantees that the functional behavior of a program cannot be tampered with even if it is loaded by and executed within a malicious environment under the control of the attacker. As such, DJS is ideal for writing JavaScript security components, such as bookmarklets, single sign-on widgets, and cryptographic libraries, that may be loaded within untrusted web pages alongside unknown scripts from arbitrary third parties. We present a tutorial of the DJS language along with motivations for its design. We show how to program security components in DJS, how to verify their defensiveness using the DJS typechecker, and how to analyze their security properties automatically using ProVerif.

JOURNAL ARTICLE

Bodin M, Chargueraud A, Filaretti D, Gardner P, Maffeis S, Naudziuniene D, Schmitt A, Smith Get al., 2014, A Trusted Mechanised JavaScript Specification, 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Publisher: Association for Computing Machinery (ACM), Pages: 87-100, ISSN: 1523-2867

CONFERENCE PAPER

Filaretti D, Maffeis S, 2014, An Executable Formal Semantics of PHP, 28th European Conference on Object-Oriented Programming (ECOOP), Publisher: SPRINGER-VERLAG BERLIN, Pages: 567-592, ISSN: 0302-9743

CONFERENCE PAPER

Bansal C, Bhargavan K, Delignat-Lavaud A, Maffeis Set al., 2013, Keys to the cloud: Formal analysis and concrete attacks on encrypted web storage, Pages: 126-146, ISSN: 0302-9743

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 find 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. © 2013 Springer-Verlag.

CONFERENCE PAPER

Bhargavan K, Delignat-Lavaud A, Maffeis S, 2013, Language-based defenses against untrusted browser origins, 22nd Usenix Security Symposium, Pages: 653-670

CONFERENCE PAPER

Bansal C, Bhargavan K, Maffeis S, 2012, Discovering Concrete Attacks on Website Authorization by Formal Analysis, 25th IEEE Computer Security Foundations Symposium (CSF), Publisher: IEEE, Pages: 247-262, ISSN: 1063-6900

CONFERENCE PAPER

Gardner P, Maffeis S, Smith G, 2012, Towards a Program Logic for JavaScript, 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Publisher: ASSOC COMPUTING MACHINERY, Pages: 31-44

CONFERENCE PAPER

Maffeis S, Rezk T, 2012, PLAS'12 - Proceedings of Programming Languages and Analysis for Security: Preface, PLAS'12 - Proceedings of Programming Languages and Analysis for Security

JOURNAL ARTICLE

Bengtson J, Bhargavan K, Fournet C, Gordon AD, Maffeis Set al., 2011, Refinement Types for Secure Implementations, ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, Vol: 33, ISSN: 0164-0925

JOURNAL ARTICLE

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

CONFERENCE PAPER

Maffeis S, Mitchell JC, Taly A, 2009, y 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

CONFERENCE PAPER

Maffeis S, Taly A, 2009, Language-Based Isolation of Untrusted JavaScript, 22nd IEEE Computer Security Foundations Symposium, Publisher: IEEE COMPUTER SOC, Pages: 77-+

CONFERENCE PAPER

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.

CONFERENCE PAPER

Maffeis S, Abadi M, Fournet C, Gordon ADet al., 2008, Code-Carrying Authorization, 13th European Symposium on Research in Computer Security, Publisher: SPRINGER-VERLAG BERLIN, Pages: 563-+, ISSN: 0302-9743

CONFERENCE PAPER

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

JOURNAL ARTICLE

Maffeis S, Gordon A, Fournet C, Bhargavan K, Bengtson Jet 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.

CONFERENCE PAPER

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

CONFERENCE PAPER

Fournet C, Gordon AD, Maffeis S, 2007, A type discipline for authorization policies, ACM Transactions on Programming Languages and Systems, Vol: 29, Pages: 25-es, ISSN: 0164-0925

JOURNAL ARTICLE

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.

CONFERENCE PAPER

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.

CONFERENCE PAPER

Maffeis S, 2007, Dynamic Web Data and Process Calculi., Bulletin of the EATCS, Vol: 93, Pages: 76-97

JOURNAL ARTICLE

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.

CONFERENCE PAPER

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

CONFERENCE PAPER

Gardner P, Maffeis S, 2005, Modelling dynamic web data, Theoretical Computer Science, Vol: 342, Pages: 104-131, ISSN: 0304-3975

JOURNAL ARTICLE

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.

CONFERENCE PAPER

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.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00342587&limit=30&person=true