Pentru desfășurarea activitaților de practică din anul I, semestrul I, studenții SLA au la dispoziție următoarele opțiuni:
- FACULTATE
Activitatea se desfășoară în facultate, profesor îndrumător: Mihăiță Drăgan.
- FACULTATE – PREGATIRE pentru CESC 2019
Se adreseaza studentilor care doresc sa participe la Campionatul European de Securitate Cibernetică, profesor îndrumător: Ruxandra Olimid.
Mai multe detalii pe pagina moodle a masterului.
- CERCETARE
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.
- COLABORARE
Studenții îsi gasesc singuri firma la care vor desfăsura activitatea de practică. In acest caz firma trebuie să semneze acordul de practică cu facultatea, iar activitatea trebuie sa fie supervizată de dl. prof. Silviu Laurențiu Vasile.
Mai multe detalii pe pagina moodle a masterului.
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.
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.
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.
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.
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:
Presenter: Traian Serbanuta.
This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter “IMP: Simple Imperative Programs”
Presenter: Traian Serbanuta.
This week we continue exploring Coq based on the Logical Foundations volume of Software Foundations, chapter “IMP: Simple Imperative Programs”
Partea a doua a cursului “Topici speciale în logică și securitate” se tine în laboratorul 321.
Instructor: Elena Burceanu (Bitdefender)
Subiect: Introducere în metode de învățare automată pentru securitate
Materiale: informatii, cursuri,
notare
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.
