Lindström’s Theorems II

Speaker: Mihai Prunescu (University of Bucharest)

Abstract: Regular logic systems which are strictly stronger than the first order predicate calculus cannot satisfy in the same time Löwenheim-Skolem for statements and compacity (Lindström 1). Effectively presented such systems cannot satisfy in the same time Löwenheim-Skolem for statements and the condition that the set of generally valid sentences is recursively enumerable (Lindström 2). We sketch the proof that uses partial isomorphisms.

References:
[1] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic. Second edition, Undergraduate Texts in Mathematics, Springer, 1996.

How to find bugs in your (x86) code: Applications that use RIVER

Speaker: Bogdan Ghimiș (University of Bucharest)

Abstract: From a security perspective, discovering bugs before shipping a product is crucial. This presentation will be about RIVER, a tool that can help us to inspect x86 binary code. This lecture will encompass two papers describing methods of finding problematic inputs: a genetic algorithm and a method using taint analysis. The genetic algorithm is used in conjunction with Apache Spark – an engine used for big data and distributed computing – to determine the inputs that provide the best code coverage. The second method uses taint analysis in order to infer which parts of the input are used by the program to determine a model with which we can generate new inputs that adhere to a certain format and that allows us to get better code coverage.

Anti-Malware Machine Learning

Speaker: Andra Băltoiu (University of Bucharest)

Abstract: In a previous seminar, we introduced Dictionary Learning (DL), a machine learning method capable of handling the requirements of IoT-related tasks, motivated by its reduced computational complexity, theoretical guarantees and its applicability to continuous retraining contexts. We now discuss the task of training different machine learning and DL models in order to identify malware and study the adaptability of the resulting models to new types of malware.

Verifying security protocols using BAN logic

Speaker: Alexandru Dragomir (University of Bucharest)

Abstract: Epistemic logics – logics aimed at reasoning about knowledge and belief – are widely considered to be suitable for modelling, analyzing and predicting vulnerabilities of security protocols. One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows, Abadi & Needham 1989), a many-sorted epistemic 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) briefly presenting the language and inference rules of BAN logic, (2) offering a presentation of the Otway-Rees, Needham-Schroeder and Kerberos protocols, and (3) analysing the aforementioned protocols using BAN logic.

Fully Homomorphic Encryption (FHE)

Speaker:  Ana Costache

Abstract:

Fully homomorphic encryption este un tip de criptare care permite manipularea datelor criptate pastrand securitatea acestora. Ana va introduce notiunea de latice, si va defini FHE. De asemenea, va vorbi despre librarii FHE si despre relevanta FHE in lumea comerciala.

Lindström’s Theorems

Speaker: Mihai Prunescu (University of Bucharest)

Abstract: Regular logic systems which are strictly stronger than the first order predicate calculus cannot satisfy in the same time Löwenheim-Skolem for statements and compacity (Lindström 1). Effectively presented such systems cannot satisfy in the same time Löwenheim-Skolem for statements and the condition that the set of generally valid sentences is recursively enumerable (Lindström 2). We sketch the proof that uses partial isomorphisms.

References:
[1] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic. Second edition, Undergraduate Texts in Mathematics, Springer, 1996.

Proudly powered by WordPress