39 results found
Arceri V, Maffeis S, 2017, Abstract Domains for Type Juggling, Publisher: ELSEVIER SCIENCE BV, Pages: 41-55, ISSN: 1571-0661
Bella G, Maffeis S, 2016, Special track on computer security (SEC), Pages: 2031-2032
Bella G, Maffeis S, 2015, 2015 Special Track on Computer Security, Pages: 2125-2126
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).
Bansal C, Bhargavan K, Delignat-Lavaud A, et al., 2014, Discovering concrete attacks on website authorization by formal analysis, Journal of Computer Security, Vol: 22, Pages: 601-657, ISSN: 0926-227X
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
Bansal C, Bhargavan K, Delignat-Lavaud A, et 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.
Bhargavan K, Delignat-Lavaud A, Maffeis S, 2013, Language-based defenses against untrusted browser origins, 22nd Usenix Security Symposium, Pages: 653-670
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
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
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
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
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, 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.
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
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 - 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., Bulletin of the 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.
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
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.
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.