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

46 results found

Alageel A, Maffeis S, 2021, Hawk-Eye: Holistic detection of APT command and control domains, Pages: 1664-1673

The high complexity and low volume of APT attacks has lead to limited insight into their behavior and to a scarcity of data, hindering research on effective detection techniques. In this paper we present a comprehensive study of the usage of domains in the context of the Command and Control (CandC) infrastructure of APTs, covering 63 APT campaigns spanning the last 13 years. We discuss the APT threat model, focusing in particular on evasion techniques, and collect an extensive dataset for studying APT CandC domains. Based on the gained insight, we propose a number of novel features to detect APTs, leveraging both semantic properties of the domains themselves and structural properties of their DNS infrastructure. We build Hawk-Eye, a system to classify domain names extracted from PCAP files, and use it to evaluate the performance of the various features we studied, and compare them to malicious domain detection features from the literature. We find that a holistic approach combining selected orthogonal features achieves the best performance, with an F1-score of 98.53% and a FPR of 0.35%.

Conference paper

Rabheru R, Hanif H, Maffeis S, 2021, DeepTective: Detection of PHP vulnerabilities using hybrid graph neural networks, Pages: 1687-1690

This paper presents DeepTective, a deep learning-based approach to detect vulnerabilities in PHP source code. DeepTective implements a novel hybrid technique that combines Gated Recurrent Units and Graph Convolutional Networks to detect SQLi, XSS and OSCI vulnerabilities leveraging both syntactic and semantic information. Experimental results show that our model outperformed related solutions on both synthetic and realistic datasets, and was able to discover 4 novel vulnerabilities in established WordPress plugins.

Conference paper

Zizzo G, Hankin C, Maffeis S, Jones Ket al., 2020, Adversarial attacks on time-series intrusion detection for industrial control systems, The 19th IEEE International Conference on Trust, Security and Privacy in Computing and Communications, Publisher: Institute of Electrical and Electronics Engineers

Neural networks are increasingly used for intrusiondetection on industrial control systems (ICS). With neuralnetworks being vulnerable to adversarial examples, attackerswho wish to cause damage to an ICS can attempt to hidetheir attacks from detection by using adversarial exampletechniques. In this work we address the domain specificchallenges of constructing such attacks against autoregressivebased intrusion detection systems (IDS) in a ICS setting.We model an attacker that can compromise a subset ofsensors in a ICS which has a LSTM based IDS. The attackermanipulates the data sent to the IDS, and seeks to hide thepresence of real cyber-physical attacks occurring in the ICS.We evaluate our adversarial attack methodology on theSecure Water Treatment system when examining solely continuous data, and on data containing a mixture of discrete andcontinuous variables. In the continuous data domain our attacksuccessfully hides the cyber-physical attacks requiring 2.87 outof 12 monitored sensors to be compromised on average. Withboth discrete and continuous data our attack required, onaverage, 3.74 out of 26 monitored sensors to be compromised.

Conference paper

Zizzo G, Hankin C, Maffeis S, Jones Ket al., 2019, Adversarial machine learning beyond the image domain, the 56th Annual Design Automation Conference 2019, Publisher: ACM Press

Machine learning systems have had enormous success in a wide range of fields from computer vision, natural language processing, and anomaly detection. However, such systems are vulnerable to attackers who can cause deliberate misclassification by introducing small perturbations. With machine learning systems being proposed for cyber attack detection such attackers are cause for serious concern. Despite this the vast majority of adversarial machine learning security research is focused on the image domain. This work gives a brief overview of adversarial machine learning and machine learning used in cyber attack detection and suggests key differences between the traditional image domain of adversarial machine learning and the cyber domain. Finally we show an adversarial machine learning attack on an industrial control system.

Conference paper

Barrere Cambrun M, Hankin C, Barboni A, Zizzo G, Boem F, Maffeis S, Parisini Tet al., 2019, CPS-MT: a real-time cyber-physical system monitoring tool for security Research, 24th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA2018), Publisher: IEEE

Monitoring systems are essential to understand and control the behaviour of systems and networks. Cyber-physical systems (CPS) are particularly delicate under that perspective since they involve real-time constraints and physical phenomena that are not usually considered in common IT solutions. Therefore, there is a need for publicly available monitoring tools able to contemplate these aspects. In this poster/demo, we present our initiative, called CPS-MT, towards a versatile, real-time CPS monitoring tool, with a particular focus on security research. We first present its architecture and main components, followed by a MiniCPS-based case study. We also describe a performance analysis and preliminary results. During the demo, we will discuss CPS-MT’s capabilities and limitations for security applications.

Conference paper

Zizzo G, Hankin C, Maffeis S, Jones Ket al., 2019, Deep Latent Defence., CoRR, Vol: abs/1910.03916

Journal article

Zizzo G, Hankin C, Maffeis S, Jones Ket al., 2019, Intrusion Detection for Industrial Control Systems: Evaluation Analysis and Adversarial Attacks., CoRR, Vol: abs/1911.04278

Journal article

Arceri V, Maffeis S, 2016, Abstract domains for type juggling, Numerical and Symbolic Abstract Domains (NSAD), Publisher: Elsevier, ISSN: 1571-0661

Web scripting languages, such as PHP and JavaScript, provide a wide range of dynamic features that makethem both flexible and error-prone. In order to prevent bugs in web applications, there is a sore need forpowerful static analysis tools. In this paper, we investigate how Abstract Interpretation may be leveragedto provide a precise value analysis providing rich typing information that can be a useful component forsuch tools.In particular, we define the formal semantics for a core of PHP that illustratestype juggling, the implicittype conversions typical of PHP, and investigate the design of abstract domains and operations that, whilestill scalable, are expressive enough to cope with type juggling. We believe that our approach can also beapplied to other languages with implicit type conversions.

Conference paper

Bella G, Maffeis S, 2016, Special track on computer security: editorial message, SAC 20116, Publisher: ACM, Pages: 2031-2032

Conference paper

Hothersall-Thomas C, Maffeis S, Novakovic C, 2015, BrowserAudit: Automated testing of browser security features, New York, NY, 2015 International Symposium on Software Testing and Analysis, Publisher: Association for Computing Machinery, 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.

Conference paper

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

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

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

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

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

Filaretti D, Maffeis S, 2014, An Executable Formal Semantics of PHP, European Conference on Object-Oriented Programming (ECOOP'14), Pages: 120-145

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, Delignat-Lavaud A, Maffeis Set al., 2013, Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage, Conference on Principles of Security and Trust (POST'13), Pages: 126-146

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

Gardner P, Maffeis S, Smith G, 2012, Towards a program logic for JavaScript, POPL 2012, Publisher: ACM, Pages: 31-44

JavaScript has become the most widely used language for clientsideweb programming. The dynamic nature of JavaScript makesunderstanding its code notoriously difficult, leading to buggy programsand a lack of adequate static-analysis tools. We believe thatlogical reasoning has much to offer JavaScript: a simple descriptionof 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 subsetof JavaScript, including challenging features such as prototypeinheritance and with. We adapt ideas from separation logic toprovide tractable reasoning about JavaScript code: reasoning abouteasy programs is easy; reasoning about hard programs is possible.We prove a strong soundness result. All libraries written in oursubset and proved correct with respect to their specifications willbe well-behaved, even when called by arbitrary JavaScript code.

Conference paper

Bansal C, Bhargavan K, Maffeis S, 2012, Discovering Concrete Attacks on Website Authorization by Formal Analysis, 25th Computer Security Foundations Symposium, Pages: 247-262, ISSN: 1940-1434

Conference paper

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, Taly A, 2009, Language-Based Isolation of Untrusted JavaScript, 22nd IEEE Computer Security Foundations Symposium, Publisher: IEEE COMPUTER SOC, Pages: 77-+

Conference paper

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

Conference paper

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, 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, 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

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

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

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

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