An introduction to BAN logic (a logic of authentication)

Speaker: Alexandru Dragomir (University of Bucharest)

Abstract: One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic [1]. BAN logic is a many-sorted modal logic used for its intuitive and compelling set of inference rules devised for reasoning about an agent’s beliefs, trust and message exchange. My presentation will focus on (1) presenting the language and inference rules of BAN logic, (2) following the original paper’s analysis of the Otway-Rees protocol, (3) presenting some objections to using BAN, and (4) discussing the problem of offering a semantics of BAN logic.

[1] M. Burrows, M. Abadi, R. Needham, A logic of authentication. Proc. Roy. Soc. London Ser. A 426, no. 1871, 233–271, 1989.

Echipa Romaniei victorioasa la ECSC2019!

Echipa României a câștigat Campionatul European de Securitate Cibernetică – European Cyber Security Challenge (ECSC 2019), desfășurat la București în perioada 9-11 octombrie 2019!

Din echipa României câștigătoare a ECSC 2019 au făcut parte și doi studenți ai FMI: Robert-Florian Dobre (anul II Informatică) și Dragoș Albăstroiu (anul II CTI), iar căpitanul echipei de anul acesta a fost Robert Vulpe (absolvent Informatică FMI 2017).

În pregătirea echipei României, un rol important l-a avut și compania certSIGN, cu care colaborăm prin stagiile de practică oferite studenților de la masterul de SLA. In anul universitar 2018-2019 profesorii masterului au organizat lecții de pregătire pentru ECSC2019, participarea la aceste lectii fiind oferită ca opțiune de practică pentru studenții SLA.

Felicitări concurenților!


Pentru desfășurarea activitaților de practică din anul I, semestrul I, studenții SLA au la dispoziție următoarele opțiuni:

    Activitatea se desfășoară în facultate, profesor îndrumător: Mihăiță Drăgan.
    Activitatea se desfăsoară la sediul firmelor cu care avem parteneriat. În acest an, vă propunem urmă toarele companii:
    – Runtime Verification Romania, subsidiara a Runtime Verification, Inc

    Studenții aleg dintre temele de cercetare propuse, activitatea este supervizată de profesorul care a propus tema. Studenții pot propune teme de cercetare, în acest caz ei trebuie sa îsi gaseasca un profesor coordonator.
    Studenții îsi gasesc singuri firma la care vor desfăsura activitatea de practică. Activitatea este supervizată de dl. prof. Silviu Laurențiu Vasile. Procedura exacta o gasiti pe pagina moodle.

Mai multe detalii pe pagina moodle a masterului.

Local Reasoning about Parametric and Reconfigurable Component-based Systems

Speaker: Radu Iosif (CNRS – VERIMAG, France)

Abstract: We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components can migrate at runtime on a physical map, whose shape and size may change. We describe such para- metric and reconfigurable architectures using resource logics, close in spirit to Separation Logic, used to reason about dynamic pointer structures. These logics support the principle of local reasoning, which is the key for writing modular specifications and building scalable verification algorithms, that deal with large industrial-size systems. Joint work with Marius Bozga and Joseph Sifakis.

Optimal Transport for (Unsupervised) Machine Learning

Speaker: Andra Băltoiu (University of Bucharest)

Abstract: After attending the “Summer School on Applied Harmonic Analysis and Machine Learning” in Genova,  Andra will give us a short introduction on Optimal Transport in the attempt of finding new prospects for the anomaly detection problem.

Anomaly Detection Reading Group: Gaussian Mixture Models

Speaker: Andrei Pătrașcu (University of Bucharest)

Abstract: We continue our adventure by investigating existing results using Gaussian Mixture Models (GMM) for anomaly detection and their adaptation to existing deep neural networks.

Required reading:

Zong, Bo, et al. “Deep autoencoding gaussian mixture model for unsupervised anomaly detection.” (2018).

Chapter 11 from Deisenroth, Marc Peter, A. Aldo Faisal, and Cheng Soon Ong. “Mathematics for Machine Learning.” (2018).

Anomaly Detection Reading Group: Distributed Online AD

Speaker: Paul Irofti (University of Bucharest)

Abstract: We continue our investigation on the task of detecting outliers in networks when dealing with big-data and investigate existing online and distributed solutions.

Required reading:

Miao, Xuedan, et al. “Distributed online one-class support vector machine for anomaly detection over networks.” IEEE transactions on cybernetics 49.4 (2018): 1475-1488.

Liu, Zhaoting, Ying Liu, and Chunguang Li. “Distributed sparse recursive least-squares over networks.” IEEE Transactions on Signal Processing 62.6 (2014): 1386-1395.