Tag Archives: Security

19/07/2017 – Talks by Mauro Tempesta, Francesco Palmarini, Heider Wahsheh, Marco Squarcina

The program of the day will be:

11.00 Mauro Tempesta
11.20 Francesco Palmarini
11.40 Heider Wahsheh
14.00 Marco Squarcina

Titles and abstracts follow:

Title: Run-time Attack Detection in Cryptographic APIs
Speaker: Marco Squarcina
Abstract:
Cryptographic APIs are often vulnerable to attacks that compromise
sensitive cryptographic keys. In the literature we find many proposals
for preventing or mitigating such attacks but they typically require to
modify the API or to configure it in a way that might break existing
applications. This makes it hard to adopt such proposals, especially
because security APIs are often used in highly sensitive settings, such
as financial and critical infrastructures, where systems are rarely
modified and legacy applications are very common. In this talk we
propose a different approach. We introduce an effective method to
monitor existing cryptographic systems in order to detect, and possibly
prevent, the leakage of sensitive cryptographic keys. The method
collects logs for various devices and cryptographic services and is able
to detect, offline, any leakage of sensitive keys, under the assumption
that a key fingerprint is provided for each sensitive key. We define key
security formally and we prove that the method is sound, complete and
efficient. We also show that without key fingerprinting completeness is
lost, i.e., some attacks cannot be detected. We discuss possible
practical implementations and we develop a proof-of-concept log analysis
tool for PKCS#11 that is able to detect, on a significant fragment of
the API, all key-management attacks from the literature.

14/07/2017 – Talk by Matus Namec

Title: Measuring Popularity of Cryptographic Libraries in Internet-Wide Scans Fingerprinting
Time: 11:00
Location: Skype call
Type: Research Result
Speaker: Matus Nemec
Abstract:
We measure the popularity of cryptographic libraries in large datasets of RSA public keys. We do so by improving a recently proposed method based on biases introduced by alternative implementations of prime selection in different cryptographic libraries. We extend the previous work by applying statistical inference to approximate a share of libraries matching an observed distribution of RSA keys in an inspected dataset (e.g., Internet-wide scan of TLS handshakes). The sensitivity of our method is sufficient to detect transient events such as a periodic insertion of keys from a specific library into Certificate Transparency logs and inconsistencies in archived datasets.

We apply the method on keys from multiple Internet-wide scans collected in years 2010 through 2017, on Certificate Transparency logs and on separate datasets for PGP keys and SSH keys. The results quantify a strong dominance of OpenSSL with more than 84% TLS keys for Alexa 1M domains, steadily increasing since the first measurement. OpenSSL is even more popular for GitHub client-side SSH keys, with a share larger than 96%. Surprisingly, new certificates inserted in Certificate Transparency logs on certain days contain more than 20% keys most likely originating from Java libraries, while TLS scans contain less than 5% of such keys.

Since the ground truth is not known, we compared our measurements with other estimates and simulated different scenarios to evaluate the accuracy of our method. To our best knowledge, this is the first accurate measurement of the popularity of cryptographic libraries not based on proxy information like web server fingerprinting, but directly on the number of observed unique keys.

30/11/2016 – Talk by Moreno Ambrosin (University of Padova)

Title: Secure and Scalable Services for the Internet of Things, and Past and Ongoing Effort in the Security of Software-Defined Networking
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Moreno Ambrosin
Abstract:
In recent years, the advent of Internet of Things (IoT) is populating the world with billions of low cost heterogeneous interconnected devices. IoT devices are quickly penetrating in many aspects of our daily lives, and enabling new innovative services, ranging from fitness tracking, to factory automation. Unfortunately, their wide use, as well as their low-cost nature, make IoT devices also an attractive target for attackers, which may exploit them to perform DoS attacks, or violate the privacy of end users. Furthermore, the potentially very large scale of IoT systems makes the use of existing security solutions unfeasible.
In this talk I will give an overview of our research effort in defining secure and scalable protocols and mechanisms for IoT services, and in particular for: (1) efficient and secure device management at large scale (commands and software distribution, and device sanity check); and (2) privacy-preservation in three representative IoT-enabled services and tasks: location-based services, advanced metering infrastructures, and decentralized consensus in a multi-agent systems. Finally, in the last part of this talk I will briefly introduce past, and ongoing research work of our group in Software-Defined Networking security.

05/10/2016 – Talk by Stefano Calzavara

Title: Theory and Practice of CSP
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Stefano Calzavara
Abstract:Content Security Policy (CSP) is a recent W3C standard introduced to prevent and mitigate the impact of content injection vulnerabilities on websites. In this talk we present a systematic, large-scale analysis of the effectiveness of the current CSP deployment, focusing on four key aspects: browser support, website adoption, correct configuration and constant maintenance. Our analysis shows that browser support for CSP is largely satisfactory, with the exception of few notable issues, but unfortunately there are several shortcomings relative to the other three aspects. CSP appears to have a rather limited deployment as yet and, more crucially, existing policies exhibit a number of weaknesses and misconfiguration errors. Moreover, content security policies are not regularly updated to ban insecure practices and remove unintended security violations. We finally discuss how formal methods are an effective tool to substantiate the claims of our empirical evaluation.

28/10/2016 – Talk by Matteo Maffei

Title: Security and Privacy for Cloud Storage
Time: 13:00
Location: Meeting room
Type: Research Result
Speaker: Matteo Maffei (Saarland University)
Abstract: Cloud storage has rapidly become a cornerstone of many IT infrastructures, constituting a seamless solution for the backup, synchronization, and sharing of large amounts of data. Putting user data in the direct control of cloud service providers, however, raises security and privacy concerns related to the integrity of outsourced data, the accidental or intentional leakage of sensitive information, the profiling of user activities and so on. Furthermore, even if the cloud provider is trusted, users having access to outsourced files might be malicious and misbehave. These concerns are particularly serious in sensitive applications like personal health records and credit score systems.
To tackle this problem, we present GORAM, a cryptographic system that protects the secrecy and integrity of outsourced data with respect to both an untrusted server and malicious clients, guarantees the anonymity and unlinkability of accesses to such data, and allows the data owner to share outsourced data with other clients, selectively granting them read and write permissions. GORAM is the first system to achieve such a wide range of security and privacy properties for outsourced storage. In the process of designing an efficient construction, we developed two new, generally applicable cryptographic schemes, namely, batched zero-knowledge proofs of shuffle and an accountability technique based on chameleon signatures, which we consider of independent interest. We implemented GORAM in Amazon Elastic Compute Cloud (EC2) and ran a performance evaluation demonstrating the scalability and efficiency of our construction.

15/09/2016 – Talk by Matus Nemec

Title: The Million-Key Question – Investigating the Origins of RSA Public Keys
Time: 10:45
Location: Meeting room
Type: Research Result
Speaker: Matus Nemec
Abstract: Can bits of an RSA public key leak information about design and implementation choices such as the prime generation algorithm? We analysed over 60 million freshly generated key pairs from 22 open- and closed source libraries and from 16 different smartcards, revealing significant leakage. The bias introduced by different choices is sufficiently large to classify a probable library or smartcard with high accuracy based only on the values of public keys. Such a classification can be used to decrease the anonymity set of users of anonymous mailers or operators of linked Tor hidden services, to quickly detect keys from the same vulnerable library or to verify a claim of use of secure hardware by a remote party.

Our broad inspection provides a sanity check and deep insight regarding which of the recommendations for RSA key pair generation are followed in practice, including closed-source libraries and smartcards. The classification of the key origins of more than 10 million RSA-based IPv4 TLS keys and 1.4 million PGP keys also provides an independent estimation of the libraries that are most commonly used to generate the keys found on the Internet.

Talk based on: https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/svenda

Title: EACirc – Advancing cryptanalytic methods through evolutionary computing
Time: 11:30
Location: Meeting room
Type: Research Result
Speaker: Matus Nemec
Abstract:Cryptographic algorithms (primitives and protocols) always have to go through elaborate testing by skilled experts to assert their overall security. The history carries many examples of serious flaws in cryptographic algorithms that rise concerns about the design and strength of the primitives.

Some automation is possible in the first phases of a cryptanalysis, e.g., by using randomness testing suites. These tools can be applied to check statistical properties of cryptographic algorithm output, to look for a deviation from randomness. Such a defect signalizes a potential flaw in the algorithm design. Yet such testing suites are limited only to predefined pattern testing for certain statistical defects, therefore others will go unnoticed.

We propose a more open approach based on an automatically generated distinguisher in the form of a multiple-output logic function (MOLF) designed by evolutionary algorithms to search for undesired statistical anomalies in the algorithm output. With contrast to the fixed sets of tests, our approach builds a distinguisher automatically, on-the-fly and adaptively to the evaluated algorithm output. This opens up new possibilities for discovering potential weaknesses that remained hidden from statistical tests and even cryptanalyst sights.

15/09/2016 – Talk by Francesco Palmarini

Title: APDU-level attacks in PKCS#11 devices
Time: 10:00
Location: Meeting room
Type: Research Result
Speaker: Francesco Palmarini
Abstract: We describe attacks on PKCS#11 devices that we successfully mounted by interacting with the low-level APDU protocol, used to communicate with the device. They exploit proprietary implementation weaknesses which allow attackers to bypass the security enforced at the PKCS#11 level. Some of the attacks leak, as cleartext, sensitive cryptographic keys in devices that were previously considered secure. We present a new threat model for the PKCS#11 middleware and we discuss the new attacks with respect to various attackers and application configurations. All the attacks presented in this paper have been timely reported to manufacturers following a responsible disclosure process

Note: The work will presented at the 19th International Symposium on Research in Attacks, Intrusions and Defenses (RAID 2016) next week.

27/07/2016 – Talk by Enrico Steffinlongo

Title:  Efficent Static Detection of Collusion Attacks in ARBAC-based Workflow Systems
Time: 14:45
Location: Acadia Lab
Type: Research Result
Speaker: Enrico Steffinlongo
Abstract:
Authorization in workflow systems is usually built on top of role-based access control (RBAC); security policies on workflows are then expressed as constraints on the users performing a set of tasks and the roles assigned to them. Unfor-tunately, when role administration is distributed and potentially untrusted users contribute to the role assignment process, like in the case of Administrative RBAC (ARBAC), collusions may take place to circumvent the intended workflow security policies. In a collusion attack, a set of users of a workflow system collaborates by changing the user-to-role assignment, so as to sidestep the security policies and run up to completion a workflow they could not complete otherwise.
In this paper, we study the problem of collusion attacks in a formal model of workflows based on stable event structures and we define a precise notion of security against collusion. We then propose a static analysis technique based on a reduction to a role reachability problem for ARBAC, which can be used to prove or disprove security for a large class of workflow systems. We also discuss how to aggressively optimise the obtained role reachability problem to ensure its tractability. Finally, we implement our analysis in a tool, WARBAC, and we experimentally show its effectiveness on a set of publicly available examples, including a realistic case study.

27/07/2016 – Talk by Marco Squarcina

Title:  Relation on ongoing PhD program
Time: 14:00
Location: Acadia Lab
Type: Research Result
Speaker: Marco Squarcina
Abstract:

The aim of this talk is to briefly report on my ongoing research activities. After presenting the accepted and in-progress papers, I will focus on the results achieved during the internship at Cryptosense in Paris where I carried out the analysis of several Java keystores (storage facilities for cryptographic keys and certificates) exposing
design and implementation weaknesses. I am currently investigating on the cracking-resistance of the keystores against brute force attacks and I plan to support my findings by implementing password cracking plugins for popular tools such as jtr or hashcat.

09/03/2016 – Talk by Stefano Calzavara

Title:  HornDroid: Practical and Sound Static Analysis of Android Applications by SMT Solving
Time: 13:30
Location: Meeting room, building Zeta
Type: Research Result
Speaker: Stefano Calzavara
Abstract:
We present HornDroid, a new tool for the static analysis of information flow properties in Android applications. The core idea underlying HornDroid is to use Horn clauses for soundly abstracting the semantics of Android applications and to express security properties as a set of proof obligations that are automatically discharged by an off-the-shelf SMT solver. This approach makes it possible to fine-tune the analysis in order to achieve a high degree of precision while still using off-the-shelf verification tools, thereby leveraging the recent advances in this field. As a matter of fact, HornDroid outperforms state-of-the-art Android static analysis tools on benchmarks proposed by the community. Moreover, HornDroid is the first static analysis tool for Android to come with a formal proof of soundness, which covers the core of the analysis technique: besides yielding correctness assurances, this proof allowed us to identify some critical corner-cases that affect the soundness
guarantees provided by some of the previous static analysis tools for Android.