Abstracts
- Speaker: Pascal Berrang (University of Birmingham)
- Title: ML-Leaks: Model and Data Independent Membership Inference Attacks and Defenses on Machine Learning Models
- Abstract: Machine learning (ML) has become a core component of many real-world applications and training data is a key factor that drives current progress. This huge success has led Internet companies to deploy machine learning as a service (MLaaS). While early demonstrations of the feasibility of such attacks had many assumptions on the adversary, we relax all previous assumptions, thereby showing that such attacks are very broadly applicable at low cost and thereby pose a more severe risk than previously thought. We present a comprehensive study on this emerging and developing threat using eight diverse datasets which show the viability of the proposed attacks across domains
- Speaker: Rizwan Asghar (University of Surrey)
- Title: From Security Analysis of Alexa’s Top One Million Domains to Cyber Resilience: Key Challenges and Future Directions
- Abstract: Due to the massive use of online activities, communication security has become a major focus of both industry and academia. Despite key advancements in communication security, potential vulnerabilities are not vanishing. To this end, we conducted a large-scale analysis of Alexa’s top one million domains to explore whether HTTPS-enabled servers are vulnerable to known attacks discovered since 1993. After unprecedented cyberattacks on NZX (New Zealand’s Exchange) and critical infrastructures, we extended the scope of our ongoing research to investigate domains vulnerable to DoS/DDoS attacks.
In this talk, security issues faced by popular domains and potential solutions will be explained. Next, we will see why organisations need to consider cyber resilience by design. Finally, we will discuss key strategies, research challenges, and future directions for achieving cyber resilience
- Speaker: Andrzej Mizera
- Title: Autonomous Trustworthy Monitoring and Diagnosis of CubeSat Health (AtMonSat)
- Abstract: CubeSat is a term coined to refer to a satellites as small as a cube with 10cm edges. Even these small satellites are recommended to comply with the ISO standards defined within the CubeSat Design Specification. CubeSats play a notable role in the New Space Economy. These spacecrafts are systems of great interest to the industry, scientific community, and government agencies as affordable facilities providing capabilities for a broad set of activities. The great success of CubeSats can be largely attributed to the “low cost and fast delivery” paradigm they introduced to the space research. Unfortunately, the new paradigm is also to be considered accountable for the high percentage of failed missions, due to the fact that CubeSat critical components are built with cheap materials and to the low-cost processes of production and verification. Furthermore, CubeSats either implement very limited Fault Detection, Isolation, and Recovery (FDIR) functionality or lack it completely. The focus of the AtMonSat project is to improve fault detection onboard CubeSats using artificial neural networks for CubeSat systems and related spacecraft where computing resources are limited.
- Speaker: Iwo Błądek
- Title: Genetic Programming for Program Synthesis Problems with Logical Constraints
- Abstract: Automatic program synthesis is increasingly used to support programmers in software development, enabling automatization for users based on simple cues or examples, and in scientific discovery. One of the alternatives to exact synthesis methods are heuristic algorithms, particularly genetic programming. While these methods do not provide guarantees of convergence towards a solution, in many instances they are able to solve the synthesis task relatively quickly. In this talk, we will present our research into using genetic programming for solving program synthesis problems with logical constraints, which is known to pose several challenges for this method.
- Speaker: Robert Kuennemann
- Title: SAPIC+: protocol verifiers of the world, unite!
- Abstract: Symbolic security protocol verifiers have reached a high degree of automation and maturity. Today, experts can model real-world protocols, but this often requires model-specific encodings and deep insight into the strengths and weaknesses of each of those tools. With SAPIC+, we introduce a protocol verification platform that lifts this burden and permits choosing the right tool for the job, at any development stage. We build on the existing compiler from SAPIC to TAMARIN, and extend it with automated translations from SAPIC+ to PROVERIF and DEEPSEC, as well as powerful, protocol-independent optimizations of the existing translation. We prove each part of these translations sound.
A user can thus, with a single SAPIC+ file, verify reachability and equivalence properties on the specified protocol, either using PROVERIF, TAMARIN or DEEPSEC. Moreover, the soundness of the translation allows to directly assume results proven by another tool which allows to exploit the respective strengths of each tool. We demonstrate our approach by analyzing various existing models.
This includes a large case study of the 5G authentication protocols, previously analyzed in TAMARIN. Encoding this model in SAPIC+ we demonstrate the effectiveness of our approach. Moreover, we study four new case studies: the LAKE-EDHOC and the Privacy-Pass protocols, both under standardization, the SSH protocol with the agentforwarding feature, and the recent KEMTLS protocol, a post-quantum version of the main TLS key exchange.
- Speaker: Emanuele D’Osualdo, MPI-SWS Saarbrücken
- Title: Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
- Abstract: In this talk, we present a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness.
Link to the paper: https://www.emanueledosualdo.com/research/papers/2020/concur-ideal-completions.html
- Speaker: Christian Esposito, University of Salerno
- Title: Blockchain-based Authentication and Trust management for the IoT-based Smart cities
- Abstract: The platforms supporting the smart city applications are rarely implemented from scratch by a municipality and/or totally owned by a single company but are more typically realized by integrating some existing ICT infrastructures thanks to a supporting platform, such as the well-known FIWARE platform. Such a multi-tenant deployment model is required to lower the initial investment costs to implement large-scale solutions for smart cities, but also imposes some key security obstacles. In fact, smart cities support critical applications demanding to protect the data and functionalities from malicious and unauthorized uses. Equipping the supporting platforms with proper means for access control is demanding, but these means are typically implemented according to a centralized approach, where a single server stores and makes available a set of identity attributes and authorization policies. Having a single root of trust is not suitable in a distributed and cooperating scenario of large-scale smart cities due to their multi-tenant deployment. In fact, each integrated system has its own set of security policies, and the other systems need to be aware of these policies, in order to allow seamless use of the same credentials across the overall infrastructure (realizing what is known as the single-sign-on). This imposes the problem of consistent and secure data replicas within a distributed system, which can be properly approached by using blockchain technology. Therefore, this seminar describes a novel solution for distributed management of identity and authorization policies by leveraging blockchain technology to hold a global view of the security policies within the system and integrating it into the FIWARE platform. In addition, IoT-based systems require trust management to implement effective authentication and authorization of nodes, as it is not possible to establish trusted connections, and/or the IoT nodes can be easily compromised. To cope with this issue, dynamic access control is required, where authorizations are granted considering security policies and node trustworthiness. However, decentralized trust management is a preferable solution, but it implies a considerable consumption of energy. Consumption is further exacerbated by the means needed to protect from attacks by the trust management entities themselves. This seminar also proposes suitable trust management for the IoT by exploiting the eventual consistency and security guarantees of blockchain.
- Speaker: Patrick Baillot
- Title: Type-based complexity analysis for a parallel process calculus
- Abstract: Some type systems have been designed to analyse statically the time
coplexity of functional languages. A natural question is whether this approach
can be extended to parallel languages. We address this problem for the
Pi-calculus, a paradigmatic calculus for parallel and concurrent computation.
In Pi-calculus, processes communicate through channels that can carry values
and channel names. We will define notions of sequential and parallel complexity
for Pi-calculus, and present a type system that provides an upper bound on the
time complexity of processes.
Based on joint work with Alexis Ghyselen (ESOP 2021)
- Speaker: Ieva Daukantas
- Title: Towards AI Security: Formal Verification of Robust Mean Estimation.
- Abstract: Trimming datasets is used as a cleaning or processing technique in many AI systems. It serves the purpose of improving the robustness of AI algorithms, so that they become less vulnerable to data related attacks. Theory states that the outliers in a data set occur with low probability, and so it follows that they can be removed without causing loss of precision in the classification result.
The talk is based on the published paper “Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation” (Ieva Daukantas, Alessandro Bruni, Carsten Schürmann), where we introduce a mechanized proof of robustness of the trimmed mean algorithm. This algorithm has high applicability as a statistical technique and can be used in many complex applications of deep learning. We combine theoretical and practical approaches: the Coq proof assistant is used to formalize the robustness of the trimmed mean algorithm and Python Naïve Bayes experiments to illustrate the applicability in AI systems.
Back to SRM presentations.
Contact
For questions and comments contact
Jun or
Peter
.
