ForSE 2020 Abstracts

Area 1 - Formal methods for Security Engineering
Full Papers Short Papers

Area 1 - Formal methods for Security Engineering

Full Papers
Paper Nr: 1
Title:

Towards a Comprehensive Solution for Secure Cryptographic Protocol Execution based on Runtime Verification
Authors:

Christian Colombo and Mark Vella
Abstract: Analytical security of cryptographic protocols does not immediately translate to operational security due to incorrect implementation and attacks targeting the execution environment. Code verification and hardware-based trusted execution solutions exist, however these leave it up to the implementer to assemble the complete solution, and imposing a complete re-think of the hardware platforms and software development process. We rather aim for a comprehensive solution for secure cryptographic protocol execution, based on runtime verification and stock hardware security modules that can be deployed on existing platforms and protocol implementations. A study using a popular web browser shows promising results with respect to practicality.
Download
Paper Nr: 2
Title:

Detection of Crawler Traps: Formalization and Implementation Defeating Protection on Internet and on the TOR Network
Authors:

Maxence Delong, Baptiste David and Eric Filiol
Abstract: In the domain of web security, websites want to prevent themselves from data gathering performed by automatic programs called bots. In that way, crawler traps are an efficient brake against this kind of programs. By creating similar pages or random content dynamically, crawler traps give fake information to the bot and resulting by wasting time and resources. Nowadays, there is no available bots able to detect the presence of a crawler trap. Our aim was to find a generic solution to escape any type of crawler trap. Since the random generation is potentially endless, the only way to perform crawler trap detection is on the fly. Using machine learning, it is possible to compute the comparison between datasets of webpages extracted from regular websites from those generated by crawler traps. Since machine learning requires to use distances, we designed our system using information theory. We used wild used distances compared to a new one designed to take into account heterogeneous data. Indeed, two pages does not have necessary the same words and it is operationally impossible to know all possible words by advance. To solve our problematic, our new distance compares two webpages and the results showed that our distance is more accurate than other tested distances. By extension, we can say that our distance has a much larger potential range than just crawler traps detection. This opens many new possibilities in the scope of data classification and data mining.
Download
Paper Nr: 3
Title:

Verifying Sanitizer Correctness through Black-Box Learning: A Symbolic Finite Transducer Approach
Authors:

Sophie Lathouwers, Maarten Everts and Marieke Huisman
Abstract: String sanitizers are widely used functions for preventing injection attacks such as SQL injections and cross-site scripting (XSS). It is therefore crucial that the implementations of such string sanitizers are correct. We present a novel approach to reason about a sanitizer’s correctness by automatically generating a model of the implementation and comparing it to a model of the expected behaviour. To automatically derive a model of the implementation of the sanitizer, this paper introduces a black-box learning algorithm that derives a Symbolic Finite Transducer (SFT). This black-box algorithm uses membership and equivalence oracles to derive such a model. In contrast to earlier research, SFTs not only describe the input or output language of a sanitizer but also how a sanitizer transforms the input into the output. As a result, we can reason about the transformations from input into output that are performed by the sanitizer. We have implemented this algorithm in an open-source tool of which we show that it can reason about the correctness of non-trivial sanitizers within a couple of minutes without any adjustments to the existing sanitizers.
Download
Paper Nr: 4
Title:

The Blockchain Potential in Computer Virology
Authors:

Joanna Moubarak, Eric Filiol and Maroun Chamoun
Abstract: This paper delves into the state of the art of computer virology formalisation then tackles the development of a new malware algorithm. It details how the work leveraged Blockchain to create an undetectable malware depicting two versions of the new malware, starting from a first naive version to achieve an advanced armoured undetectable k-ary malware that leverages decentralized storage namely IPFS. The detection of the new malware algorithm has been proven NP-complete.
Download
Paper Nr: 6
Title:

Android Run-time Permission Exploitation User Awareness by Means of Formal Methods
Authors:

Fausto Fasano, Fabio Martinelli, Francesco Mercaldo and Antonella Santone
Abstract: Our mobile devices store a lot of sensitive and critical information. Moreover, considering the ability of smartphones and tables to detect the position and to record audio, it is not absolutely an exaggeration to admit that potentially our devices can easily spy on us. The ability to perform these crucial tasks must be granted by the user at the time of their first use by accepting the so-called permissions. The problem is that in Android, once these permissions are granted, the application can always use them without notifying the user. In this paper, we propose a methodology, based on formal methods, aimed to detect the exact point in the code (in term of package, class and method) of an Android application where a permission is invoked at run-time. Moreover we design a tool able to advise the user whether a permission is invoked, in this way the user can be informed about the application behaviour.
Download
Paper Nr: 9
Title:

Analysis of Security Attacks in Wireless Sensor Networks: From UPPAAL to Castalia
Authors:

Cinzia Bernardeschi, Gianluca Dini, Maurizio Palmieri and Francesco Racciatti
Abstract: Wireless Sensor Networks (WSNs) are particularly prone to security attacks. However, it is well-known that perfect security is not achievable. Therefore, it is important to identify threats and evaluate their severity, for prioritizing the security countermeasures to be adopted, even since design time. In this work, we propose an approach that binds formal methods and network simulation for assessing the effects of security attacks on WSN applications from design time, starting from the abstract model of the system. Formal methods make it possible to build abstract system models and state properties of general validity, but cannot provide any concrete measurement regarding the network and the application. On the other hand, network simulators can provide precise and realistic information about simulated scenarios only. As a proof of concept, we design and prototype an application-level communication protocol, which is simulated both on attack free and attack scenarios. First, the protocol’s formal properties are specified and proved via UPPAAL. Then, the resulting UPPAAL model is used to automatically generate a network model for the WSN simulator Castalia. Finally, the network model is simulated against attack free and attack scenarios, for gathering realistic information about the protocol behavior and performance.
Download
Paper Nr: 10
Title:

Accidental Sensitive Data Leaks Prevention via Formal Verification
Authors:

Madalina G. Ciobanu, Fausto Fasano, Fabio Martinelli, Francesco Mercaldo and Antonella Santone
Abstract: Our mobile devices, if compared to their desktop counterpart, store a lot of sensitive and private information. Considering how easily permissions to sensitive and critical resources in the mobile environment are released, for example in Android, sometimes the developer unwittingly causes the leakage of sensitive information, endangering the privacy of users. Starting from these considerations, in this paper we propose a method aimed to automatically localise the code where there is the possibility of information leak. In a nutshell, we discuss a method aimed to check whether a sensitive information is processed in a way that violates specific rules. We employ code instrumentation to annotate sensitive data exploiting model checking technique. To show the effectiveness of the proposed method a case study is presented.
Download
Short Papers
Paper Nr: 7
Title:

Comparing Machine Learning Techniques for Malware Detection
Authors:

Joanna Moubarak and Tony Feghali
Abstract: Cyberattacks and the use of malware are more and more omnipresent nowadays. Targets are as varied as states or publicly traded companies. Malware analysis has become a very important activity in the management of computer security incidents. Organizations are often faced with suspicious files captured through their antiviral and security monitoring systems, or during forensics analysis. Most solutions funnel out suspicious files through multiple tactics correlating static and dynamic techniques in order to detect malware. However, these mechanisms have many practical limitations giving rise to a new research track. The aim of this paper is to tackle the use of machine learning algorithms to analyze malware and expose how data science is used to detect malware. Training systems to find attacks allows to develop better protection tools, capable of detecting unprecedented campaigns. This study reveals that many models can be employed to evaluate their detectability. Our demonstration results illustrates the possibility to analyze malware leveraging several machine learning (ML) algorithms comparing them.
Download
Paper Nr: 5
Title:

Bank Credit Risk Management based on Data Mining Techniques
Authors:

Fabio Martinelli, Francesco Mercaldo, Domenico Raucci and Antonella Santone
Abstract: In last years, data mining techniques were adopted with the aim to improve and to automatise decision-making processes in a plethora of domains. The banking context, and especially the credit risk management area, can benefit by extracting knowledge from data, for instance by supporting more advanced credit risk assessment approaches. In this study we exploit data mining techniques to estimate the probability of default with regard to loan repayments. We consider supervised machine learning to build predictive models and association rules to infer a set of rules by a real-world data-set, reaching interesting results in terms of accuracy.
Download