Speaker: Ionuţ Ţuţu (Royal Holloway, University of London)
Abstract: We propose a hybrid-dynamic first-order logic as a formal
foundation for specifying and reasoning about reconfigurable
systems. As the name suggests, the formalism we develop extends
(many-sorted) first-order logic with features that are common to
hybrid and to dynamic logics. This provides certain key advantages for
dealing with reconfiguration, such as: (a) a signature of nominals,
including operation and relation symbols, that allows references to
specific possible worlds / system configurations – as in the case of
hybrid logics; (b) distinguished signatures of rigid and flexible
symbols, where the rigid symbols are interpreted uniformly across
possible worlds – this supports a rigid form of quantification, which
ensures that variables have the same interpretation regardless of the
possible world where they are evaluated; (c) hybrid terms, which
increase the expressive power of the logic in the context of rigid
symbols; and (d) modal operators over dynamic-logic actions, which are
defined as regular expressions over binary nominal relations. In this
context, we advance a notion of hybrid-dynamic Horn clause and develop
a series of results that lead to an initial-semantics theorem for the
Horn-clause fragment of hybrid-dynamic first-order logic.
Speaker: Ruxandra Olimid (University of Bucharest)
Abstract: Short (crypto) introduction in Blockchain. Mostly a reading group, discussing the original bitcoin paper: https://bitcoin.org/bitcoin.pdf
Speaker: Mihai Prunescu (University of Bucharest)
Abstract: We discuss different implications of the negative answer of Hilbert’s Tenth Problem: the exponential Diophantine equation over ℕ and ℚ, the minimal number of variables which lead to an undecidable problem over ℤ, the homogeneous Diophantine problem over ℤ.
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. I will assume knowledge of the basics of BAN logic and focus on presenting and analyzing the Needham-Schroeder and Kerberos protocols using this particular logical framework. Consequently, I will highlight some of the pros and cons of using BAN logic in verifying security protocols.
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.
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.
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.
Bursa de merit anul I: Cir Constantin
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.
