SECURITY & APPLIED LOGIC

BLOCKCHAIN - More than a buzzword
2020-03-02 18:30 - 20:00 UTC | Facultatea de Matematica si Informatica, sala 219
Title: BLOCKCHAIN – More than a buzzword
Speaker: Ionut-Daniel Dobos (MBN Technologies)

Abstract: In this presentation we will take a look at the concept of a blockchain as a mean to hold historical transactional data (while maintaining all the core concepts of Cryptography) and moreover, to see how IPFS uses such approaches to ensure a way of general data storage with the same capabilities. We will choose the Ethereum network as a use case for the first topic, taking a deeper look into the upcoming Casper update for the consensus mechanism, introducing the Proof of Stake paradigm.

A quantitative analysis of the “Lion-Man” game
2020-02-27 10:00 - 12:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Ulrich Kohlenbach (Technische Universität Darmstadt)
Title: A quantitative analysis of the “Lion-Man” game
Abstract: We analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a discrete lion and man game with an ε-capture criterion. We prove that in uniformly convex bounded domains the lion always wins and, using ideas stemming from proof mining, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis, we study the relation among different convexity properties in the setting of geodesic spaces.
Joint work with Genaro López-Acedo and Adriana Nicolae.

References:
[1] U. Kohlenbach, G. López-Acedo, A. Nicolae, A quantitative analysis of the “Lion-Man” game. arXiv:1806.04496 [math.MG], 2019. Submitted.

Challenges in Banking
2020-01-30 08:30 - 10:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Horia Velicu (BRD – Groupe Societe Generale)

Abstract: Presentation of topics of interest for 2020, objectives and data available at BRD. Proposals for the themes for the applied research institute that will be sponsored this year. Presentation of the new BRD AI Hub.

Off-the-Record Communication (OTR) si CryptoGo (joc de carti de criptografie)
2019-12-19 18:30 - 20:00 UTC | Facultatea de Matematica si Informatica, amf.2 (Pompei)
Title: Off-the-Record Communication (OTR)
Speaker: Mihail-Iulian Plesa

Abstract: Off-the-Record Communication (OTR) este un protocol care modealeaza o discutie dintre doua entitati, care ar trebui sa satisfaca anumite proprietati de securitate. Vom vorbi despre proprietatile acestui tip de comunicatie si despre cum pot fi acestea implementate in mediul online. Vom discuta apoi despre protocolul OTR integrat in Signal si cum anume difera acesta fata de versiunea originala.
Nota: Prezentarea va fi urmata de o sesiune de joc CryptoGo – joc de carti educational pentru criptografie.
Mai multe informatii aici.

First-order logic and vagueness
2019-12-19 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Marian Calborean (University of Bucharest)

Abstract: The Sorites paradox is usually studied as a propositional paradox. However, the general form of the Sorites is second-order, with three main features. It doesn’t contain any arbitrary parameters. It can be used to generate the propositional Sorites by appropriate replacement of the second-order premise with arbitrary clauses. Finally, it is generally nonfirstorderizable, relying on the notion of transitive closure of a relation. However, it can be expressed in FOL with a finite upper bound on the elements of the relation. This leads to a definition of vagueness in classical FOL, using the interplay between a total preorder and a monadic predicate. A notational extension of FOL will introduce a vague structure formed by the predicate (e.g.tall), the broad predicate (e.g. broadly tall) and the strict predicate (e.g. strictly tall). It allows the failure of a weak non-contradiction (e.g. ‘Some men are both broadly tall and broadly short’), the failure of a weak LEM (e.g. ‘Some men are neither strictly tall nor strictly short`), and the truth of a non-paradoxical tolerance (e.g. ‘If a person of n cm is strictly tall, a person of n-1 cm is broadly tall’).
References:
[1] P. Cobreros, P. Egré, D. Ripley, R, Van Rooij, Tolerant, Classical, Strict, Journal of Philosophical Logic 41 (2019), 347-385.
[2] D. Graff, Shifting Sands: An Interest-Relative Theory of Vagueness, Philosophical Topics 28 (2000), 45-81.
[3] U. Keller, Some remarks on the definability of transitive closure in first-order logic and Datalog, Internal report, Digital Enterprise Research Institute (DERI), University of Innsbruck, 2004.
[4] K.G. Lucey, he ancestral relation without classes, Notre Dame Journal of Formal Logic 20 (1979), 281-284.

Operational Semantics of Security Protocols II
2019-12-12 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Ioana Leustean (University of Bucharest)

Abstract: We continue our presentation on operational semantics of security protocols, as developed in:
C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Springer, 2012.

Executarea, detecţia și prevenţia atacurilor de tip R.O.P
2019-12-12 08:30 - 11:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Sorin-Gabriel Radu (University of Bucharest)

Abstract: Va fi prezentată o versiune extinsă a lucrări de licență ce va prezenta concepte de Return Orientated Programming, o tehnică de reciclare și combinare a bucăților de cod existent, curat, astfel încât cod nou, nedorit, în general de tip malware, să fie executat.

Operational Semantics of Security Protocols
2019-11-21 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Ioana Leustean (University of Bucharest)

Abstract: After a brief overview of the formal methods used for analyzing security protocols, we will focus on the operational semantics developed in:
C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Springer, 2012.

Anomaly Detection Reading Group: Anomaly Detection by Unmasking
2019-11-21 08:30 - 10:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Marius Popescu (University of Bucharest)

Abstract: We continue our adventure by investigating existing natural language processing results that deal with unmasking authorship and their application to anomaly detection.
Required reading:
M. Koppel, J. Schler, and E. Bonchek-Dokow. Measuring Differentiability: Unmasking Pseudonymous Authors. Journal of Machine Learning Research, 8:1261–1276, 2007.
T.R. Ionescu, S. Smeureanu, B. Alexe, and M. Popescu. Unmasking the abnormal events in video. In Proceedings of the IEEE International Conference on Computer Vision (pp. 2895-2903), 2017.

ManyVal 2019
2019-11-01 09:30 - 2019-11-03 13:00 UTC
In perioada 1-3 noiembrie organizam workshop-ul international ManyVal 2019, dedicat in special cercetarilor in logica cu mai multe valori. Editia actuala beneficiaza si de participarea unor filozofi-logicieni de marca. Pentru mai multe detalii puteti consulta pagina manifestarii:

https://cs.unibuc.ro/events/manyval2019/

Persoanele inregistrate vor primi kit-ul workshop-ului si vor putea participa la mesele si activitatile sociale anuntate.

Participarea la prezentari NU presupune plata taxei de inregistrare, iar anumite materiale (program, carte de abstracte) vor putea fi descarcate de pe pagina ManyVal 2019.

An introduction to BAN logic (a logic of authentication)
2019-10-24 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
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.
References:
[1] M. Burrows, M. Abadi, R. Needham, A logic of authentication. Proc. Roy. Soc. London Ser. A 426, no. 1871, 233–271, 1989.

Optimal Transport for (Unsupervised) Machine Learning
2019-09-20 10:00 - 23:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
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.

Local Reasoning about Parametric and Reconfigurable Component-based Systems
2019-09-19 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala Google
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.

Anomaly Detection Reading Group: Gaussian Mixture Models
2019-08-30 10:00 - 23:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
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
2019-08-21 10:00 - 23:30 UTC | Facultatea de Matematica si Informatica, sala Google
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.

Anomaly Detection Reading Group: Graph Classification
2019-08-08 10:00 - 23:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala Google
Speaker: Andra Băltoiu (University of Bucharest)

Abstract: We continue our investigation on the task of detecting outliers in networks, by looking at the concept of signal variation on a graph.
Required reading:
A. Sandryhaila and J. M. F. Moura, “Classification via regularization on graphs,” 2013 IEEE Global Conference on Signal and Information Processing, Austin, TX, 2013, pp. 495-498.
S. Chen, A. Sandryhaila, J. M. F. Moura and J. Kovačević, “Signal Recovery on Graphs: Variation Minimization,” in IEEE Transactions on Signal Processing, vol. 63, no. 17, pp. 4609-4624, Sept.1, 2015.

Anomaly Detection Reading Group: Deep RPCA
2019-08-01 10:00 - 23:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Speaker: Andrei Pătrașcu (University of Bucharest)

Abstract: We continue our adventure by investigating existing results with Robust Principal Component Analysis (RPCA) and its adaptation to existing deep neural networks.
Required reading:
ZHOU, Chong; PAFFENROTH, Randy C. Anomaly detection with robust deep autoencoders. In: Proceedings of the 23rd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. ACM, 2017. p. 665-674.
CANDÈS, Emmanuel J., et al. Robust principal component analysis?. Journal of the ACM (JACM), 2011, 58.3: 11.

Anomaly Detection Reading Group: Deep OC-SVM
2019-07-25 10:00 - 23:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Speaker: Andrei Pătrașcu (University of Bucharest)

Abstract: Recent empirical results confirm that one-class (OC) classification methods remain among the most important learning strategies for anomaly detection. In this seminar, we will technically describe in detail multiple basic OC schemes such as OC-SVM and SVDD and their deep variants, in order to identify room of improvements or generalization directions towards the graph anomaly detection context.

Dynamic Code Analysis
2019-05-30 17:00 - 18:00 UTC
Speaker: Radu Velea (BitDefender)

Abstract: Static code analysis methods have the advantage of providing deterministic and reliable results. Malware has evolved beyond the point where simple pattern matching algorithms or signatures can provide adequate levels of protection. To respond to new threats we have to look at other hidden aspects such as execution behavior and fight evasive techniques by performing dynamic code analysis. This presentation discusses how to do this using runtime emulation and describes the existing challenges for the most popular architectures and executable file formats.

Protocols in Dynamic Epistemic Logic
2019-05-30 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Alexandru Dragomir (University of Bucharest)

Abstract: Dynamic epistemic logics are useful in reasoning about knowledge and certain acts of learning (epistemic actions). However, not all epistemic actions are allowed to be executed in an initial epistemic model, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to two accounts of protocols in DEL: one based on [1], and the second on [2].
References:
[1] T. Hoshi, Epistemic dynamics and protocol information, PhD thesis, Stanford University, 2009.
[2] Y. Wang, Y. Epistemic Modelling and Protocol Dynamics, PhD thesis, University of Amsterdam, 2010.

House of clouds – sau cum sa auditezi un sistem in cloud
2019-05-22 18:30 - 19:30 UTC | Facultatea de Matematica si Informatica, sala 219
Speaker: Georgel Gheorghe este absolvent al facultatii de Electronica, Telecomunicatii si Tehnologia a informatiei. Este membru ISACA si detine certificari precum CISA (Certified Information Systems Auditor), CGEIT (Certified in the Governance of Enterprise IT) si CRISC (Certified in Risk and Information Systems Control).
Are o experienta de peste 11 ani in audit si consultanta in industrii de tipologii diferite (servicii financiare, retail, productie, telecomunicatii, energie) cu proiecte precum: evaluari ale mediilor IT&IS, audituri de conformitate, evaluari ale configurarilor de securitate, managementul vulnerabilitatilor, managementul continuitatii afacerii, managementul schimbarilor.
Dupa mai multi ani petrecuti in Deloitte, Ericson si Mazars, s-a alaturat unei noi echipe unde cunostintele si experienta sa sunt o baza solida pentru identificarea unor solutii potrivite pentru noile provocari digitale.

Abstract: Prezentarea propusa, House of clouds – sau cum sa auditezi un sistem in cloud, va aborda aspecte relevante ce tin de intelegerea si delimitarea sistemelor in scop, identificarea riscurilor si selectarea masurilor de control necesare.
In introducere, Gratiela Magdalinoiu (presedinte ISACA Romania) va face o scurta prezentare ISACA Romania.

An introduction to hybrid-dynamic first-order logic
2019-05-16 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
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.

Anti-Malware Machine Learning
2019-04-18 08:30 - 10:00 UTC | Facultatea de Matematica si Informatica, sala 202
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.

Blockchain - Intro
2019-04-17 18:30 - 19:30 UTC | Facultatea de Matematica si Informatica, sala 219
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

Around Hilbert's Tenth Problem
2019-04-11 10:00 - 12:00 UTC
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 ℤ.

How to find bugs in your (x86) code: Applications that use RIVER
2019-04-04 09:00 - 10:00 (Europe/Helsinki) | Facultatea de Matematica si Informatica, sala 202
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.

Verifying security protocols using BAN logic - Part 2
2019-04-04 08:30 - 09:00 (Europe/Helsinki) | Facultatea de Matematica si Informatica, sala 202
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.

Lindström's Theorems II
2019-03-28 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala 202
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.

Verifying security protocols using BAN logic
2019-03-21 08:30 - 10:00 UTC | Facultatea de Matematica si Informatica, sala 202
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)
2019-03-20 18:30 - 19:30 UTC | Facultatea de Matematica si Informatica, sala 219
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.
