SECURITY & APPLIED LOGIC

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)
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)
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)

How to find bugs in your (x86) code; RIVER tool - current state and future
2018-12-13 08:30 - 10:00 UTC
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)
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)
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)
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.
