SECURITY & APPLIED LOGIC

Lindström's Theorems
2019-03-14 10: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.

Identificarea metodelor de automatizare a etapelor de analiza cuprinse in cadrul procedurilor de Securitate/ raspuns la incidente cibernetice utilizate in cadrul unui SOC
2019-03-07 08:30 - 10:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Alin Puncioiu (Secureworks)

Abstract: In cadrul prezentarii vom prezenta cateva fluxuri de lucru executate manual in momentul de fata pe parcursul fazelor de raspuns la incidente cibernetice.

Functional Encryption (FE)
2019-03-06 18:30 - 19:30 UTC
Speaker: Radu Titiu

Abstract:
Functional Encryption (FE) este o primitiva criptografica moderna care generalizeaza notiunea de criptografie cu cheie publica in felul urmator. In mod normal algoritmul de decriptare se foloseste de cheia secreta pentru a recupera intreg mesajul criptat cu cheia publica. FE permite o decriptare controlata a mesajului: detinatorul cheii secrete K poate sa produca alta cheie secreta K_f asociata unei functionalitati f. Folosind cheia K_f un utilizator poate sa obtina f(mesaj) si nimic mai mult. O astfel de primitiva criptografica ar putea fi utilizata de un spital care tine datele pacientilor criptate dar care poate totusi oferi acces cercetatorilor la anumite statistici care ar putea ajuta la intelegerea anumitor boli. Toate acestea sunt posibile fara a divulga informatii despre pacienti.
In aceasta prezentare Radu va explica detaliat ce inseamna Functional Encryption si posibile aplicatii. De asemenea, va exemplifica conceptul printr-o constructie pentru o clasa restransa de functionalitati [2] si va vorbi despre cerintele de securitate pe care le satisface aceasta constructie.
Referinte:
[1] https://link.springer.com/chapter/10.1007%2F978-3-319-70500-2_8
[2] https://eprint.iacr.org/2015/608.pdf

An introduction to BAN logic (a logic of authentication)
2019-02-28 10:00 - 12:00 UTC
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 (Burrows, Abadi & Needham 1989), 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.

The hybridization of many-sorted polyadic modal logic
2019-02-28 10:00 - 12:00 UTC
Speaker: Natalia Moangă (University of Bucharest).
Abstract: Hybrid logics are obtained by enriching modal logics with nominals and state variables, that directly refer the individual points in a Kripke model. In the present work we develop a hybrid version on top of our many-sorted polyadic logic, previously defined. Our system has nominals and state variables on each sort, as well as binders that act like the universal and the existential quantfiers on state variables. In doing this, we follow various approaches for hybrid modal logic, especially the work of Blackburn and Tsakova.

Security via user behavior
2019-02-21 08:30 - 22:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Speaker: Cezara Benegui (University of Bucharest).

Abstract: The presentation will be based on earlier research done on user behaviour understanding and detection, learning it using machine learning and artificial intelligence and further information about how user behaviour can be used to improve the security of software applications. Also, the presentation will include information about biometrics like keystroke timings, mouse dynamics, scrolling and tapping behaviour, software usage behaviour, what is their importance and how can they be used for anomaly/intrusion detection or for identifying and targeting users on a wide variety of other applications.

Security aspects for blockchain
2019-02-21 08:30 - 10:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Speaker: Andreea Elena Panait (University of Bucharest).

Abstract: The presentation will include introductive notions about blockchain, the main types of attacks on the blockchain network and possible countermeasures, attack examples that occurred during the years, blockchain implementation examples and possible domains where blockchain can be used.

Criptosistemul lui McEliece, dupa 40 de ani de criptanaliza
2019-02-18 18:30 - 20:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 220, Strada Academiei 14, Bucuresti, Bucuresti, Romania
Speaker: Vlad Dragoi (Univ. Aurel Vlaicu Arad)

Abstract:
Aceasta prezentare are ca scop descrierea principalelor solutii de criptare asimetrica cu ajutorul codurilor corectoare de erori. Vom incerca sa discutam cat mai multe aspecte legate de aceste protocoale, cum ar fi: natura codurilor folosite in acest context, complexitatea algoritmilor de criptare si decriptare, securitatea protocolului (distinguisher, message recovery attacks, key recovery attacks). Daca timpul ne permite vom incerca sa detaliem una dintre variante, de exemplu McEliece textbook cu codurile Goppa binare.

Verification of strategic properties for the Prêt-À-Voter protocol using Tamarin (joint work with Wojtek Jamroga and Damian Kurpiewski)
2019-02-07 08:30 - 10:00 UTC | Facultatea de Matematica si Informatica, sala Google
Speaker: Catalin Dima (Université Paris-Est Créteil)

Abstract:
We report on the verification of anonymity and coercion-freeness properties of the Prêt-À-Voter electronic voting protocol using the Tamarin tool for symbolic verification of security properties. Our approach is to generate many models corresponding with each choice of attacker actions (i.e. attacker strategies) and check, on each model, a “trace equivalence” lemma modeling the fact that the attacker does not distinguish between a trace in which the coerced voter has obeyed the orders, from a trace in which the voter has ignored the coercion. This seems to be the only approach available in Tamarin for modeling epistemic knowledge, a notion necessary for encoding anonymity. The results are far from encouraging since many false negatives or positives are obtained, necessitating model adaptations which cannot be done automatically, and when correct results are obtained the running times are prohibitive. Our conclusions point the need for theory and tool improvement in which equational and rewriting logics be combined with strategy logics.

The frontier between decidability and undecidability for logics for strategic reasoning in the presence of imperfect information
2019-01-31 10:00 - 12:00 UTC | Facultatea de Matematica si Informatica, sala Google
Speaker: Catalin Dima (Université Paris-Est Créteil.)

Abstract:
The last 15-20 years have seen a number of logical formalisms that focus on strategic reasoning. These logics aim at giving specification languages for various multi-agent game structures, in which agents have adversarial or cooperative objectives which may be qualitative or quantitative and may have various types of imperfect information. The presence of imperfect information raises a particular difficulty in that many games cannot be solved algorithmically, as well as their corresponding logical formalisms. In this tutorial I will review some techniques for proving that the Alternating-time Temporal Logic has an undecidable model-checking problem, but this problem becomes decidable when considering memoryless strategies, coalitions with distributed knowledge, hierarchical knowledge and public or coalition-public announcements. I will also give a short introduction to the model-checking tool MCMAS which relies on the memoryless semantics for ATL with imperfect information, and the problems that arise when implementing the model-checking algorithms for this case.

Making Obsolete Malware Viable with Packing
2019-01-17 08:30 - 10:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Mihai Stancu

Abstract:
The security trend today is to stop security threats even before they
arrive on the target machine or system.
With that in mind we will explore, what packers are and what they do to
transform original malicious code in into something that is much harder to
confidently mark as a threat.
This talk will be focused on executables in the PE format running on the
Windows platform and during the presentation we will form a basic
understanding of the executable structure, packing technique, and other
anti-dumping and anti-debug techniques work to protect and run the original
payload.

Logical Foundations: Simple Imperative Programs - variables and commands
2018-12-20 18:00 - 20:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Presenter: Traian Serbanuta.

This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter “IMP: Simple Imperative Programs”

The finitary content of sunny nonexpansive retractions
2018-12-20 10:00 - 12:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Andrei Sipoș (TU Darmstadt & IMAR).

The goal of proof mining is to extract quantitative information out of proofs in mainstream mathematics which are not necessarily fully constructive. Often, such proofs make use of strong mathematical principles, but a preliminary analysis may show that they are not actually needed, so the proof may be carried out in a system of strength corresponding roughly to first-order arithmetic. Following a number of significant advances in this vein by Kohlenbach in 2011 and by Kohlenbach and Leuștean in 2012, we now tackle a long-standing open question: the quantitative analysis of the strong convergence of resolvents in classes of Banach spaces more general than Hilbert spaces.
This result was proven for the class of uniformly smooth Banach spaces by Reich in 1980. What we do is to analyze a proof given in 1990 by Morales, showing that adding the hypothesis of the space being uniformly convex, and thus still covering the case of L^p spaces, can serve to eliminate the strongest principles used in the proof by way of a modulus of convexity for the squared norm of such spaces. A further procedure of arithmetization brings the proof down to System T so the proper analysis may proceed. After obtaining a non-effective realizer of the metastability statement, this is majorized in order to obtain the desired rate. Subsequent considerations calibrate this bound to T_1. It particular, this result completes some analyses that had previously been obtained only partially, yielding rates of metastability within the above-considered class of Banach spaces for the Halpern and Bruck iterations.
These results are joint work with Ulrich Kohlenbach.

References:
[1] U. Kohlenbach, A. Sipoș, The finitary content of sunny nonexpansive retractions. arXiv:1812.04940 [math.FA], 2018. Preprint. Up-to-date version at: https://www2.mathematik.tu-darmstadt.de/~kohlenbach/resolvent-paper.pdf

Logical Foundations: Simple Imperative Programs
2018-12-13 18:00 - 20:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202

How to find bugs in your (x86) code; RIVER tool - current state and future
2018-12-13 08:30 - 10:00 UTC | Facultatea de Matematica si Informatica, sala 202
Speaker: Ciprian Păduraru

Abstract:
Even with access to the source code of a program, it is not easy to reverse engineer a program to find inputs for specific programs. This presentation starts with a practical walkthrough over classic methods for automating software testing, such as fuzz testing, symbolic and concolic execution. Then, a tool named RIVER is presented in its current state, together with the technical plans for improving it to achieve at least the same features set with similar tools such as KLEE. By using its reversible execution capabilities, and advanced tracing support, we think that by putting efforts in the implementation plan described in the presentation, we can obtain improved test coverage in relation to resources consumed. Research ideas for various parts including RIVER symbolic/concolic execution, tracers improvements, and combining these techniques with machine learning will be presented.

Logical Foundations: Total and Partial Maps
2018-12-06 18:00 - 20:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Speaker: Miriam Costan.

This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter “Total and Partial Maps”

Classical and quantum degrees of truth: a new look at the effects of a Hilbert space
2018-12-06 10:00 - 12:00 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Speaker: Roberto Giuntini (University of Cagliari).

We investigate certain Brouwer-Zadeh lattices that serve as abstract counterparts of lattices of effects in Hilbert spaces under the spectral ordering. These algebras, called PBZ∗-lattices, can also be seen as generalisations of orthomodular lattices and are remarkable for the collapse of three notions of “sharpness” that are distinct in general Brouwer-Zadeh lattices. We investigate the structure theory of PBZ∗-lattices and their reducts; in particular, we prove some embedding results for PBZ∗-lattices and provide an initial description of the lattice of PBZ∗-varieties.

Machine Learning Framework for Security Applications
2018-11-29 08:30 - 10:30 (Europe/Bucharest) | Facultatea de Matematica si Informatica, sala 202
Speaker: Paul Irofti (University of Bucharest).

Machine learning helps us tackle large and apparently intractable optimization problems. Even though neural networks are by far the most popular choice in the field, we focus on dictionary learning (DL) for sparse representations (SR) instead. Our preference is motivated by the much simpler model that provides faster methods with a solid theoretical background, understanding and interpretability.
In fact it has been recently shown that the forward pass inside neural networks is equivalent to performing sparse representation. Thus performing dictionary learning can be interpreted as a backward pass on a much simpler and smaller model. This relaxation comes with a small performance hit in exchange for the large reduction in algorithm complexity.
Our talk will focus on adapting DL to Big Data conditions, DL classification and the problem of malware identification, nomaly detection, online DL and Internet of Things applications.
