Abstracts
- 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: 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.
- 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: 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: 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
Back to SRM presentations.
Contact
For questions and comments contact
Matteo or
Masoud
.
