|
|
Lundi 29 Juin
Heure: |
12:15 - 13:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
BE-PUM: A tool of Binary Emulation for Pushdown Model generation |
Description: |
Quan Thanh Tho In this talk, we present the tool BE-PUM (Binary Emulation for PUshdown Model generation) for binary analysis. As suggested by its name, BE-PUM generates pushdown model, which is considered as a control flow graph (CFG) combined with a memory execution model. BE-PUM also introduces a concolic approach in order to generate CFG in a more precise manner. As such, BE-PUM is able to handle various popular obfuscation techniques of malwares, such as indirect jump or self- modification code. In experiments, we are able to produce models for around 1700 samples of real malware. Compared to JakStab and IDA Pro, two state-of-the-art tools in this field, BE-PUM shows better tracing ability, sometimes with significant differences. |
Heure: |
14:00 - 15:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Annotation et exploration de textes de spécialité - fragments d'une expérience |
Description: |
François Lévy, Sylvie Szulman Nous avons (ré)écrit un outil de manipulation conjointe d'annotations et de textes annotés, Omtat (One More Textual Annotation Tool) qui permet de visualiser les annotations et d'en ajouter, Les annotations, inspirées de Brat (Brat rapid annotation tool) peuvent porter sur une zone discontinue et qualifier des annotations-arguments. Un moteur de requêtes permet d'extraire et d'exploiter des ensembles de documents, phrases et annotations. Les premiers tests portent sur des textes de biologies et sur des textes juridiques, pour lesquels nous avons créé quelques types d'annotations spécialisées. Nous en profiterons pour dire en quoi spécialiser les annotations en tenant compte du domaine nous parait utile et tenter de convaincre que les résultats peuvent être intéressants. |
Jeudi 2 Juillet
Heure: |
12:30 - 13:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Solving the quadratic shortest path problem |
Description: |
Borzou Rostami Finding the shortest path in a directed graph is one of the most important combinatorial optimization problems, having applications in a wide range of fields. In its basic version, however, the problem fails to represent situations in which the value of the objective function is determined not only by the choice of each single arc, but also by the combined presence of pairs of arcs in the solution. In this paper we model these situations as a Quadratic Shortest Path Problem, which calls for the minimization of a quadratic objective function subject to shortest-path constraints. We prove strong NP-hardness of the problem and analyze polynomially solvable special cases, obtained by restricting the distance of arc pairs in the graph that appear jointly in a quadratic monomial of the objective function. Based on this special case and problem structure, we devise fast lower bounding procedures for the general problem and show computationally that they clearly outperform other approaches proposed in the literature in terms of their strength. |
Heure: |
14:30 - 15:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Action synthesis for branching time logic: theory and applications |
Description: |
Micha? Knapik Action-Restricted Computation Tree Logic (ARCTL) is a simple extension of CTL, proposed by Pecheur and Raimondi, where the actions allowed along the considered runs can be explicitly indicated by path selectors. ARCTL allows to express properties such as "a safe state is unavoidable for every path built from Forward and Left actions", denoted by AF{Forward,Safe}safe. By replacing the concrete sets of actions with free variables we obtain a parametric version of the logic pmARCTL, where properties such as AF{X}safe are allowed, where X is a parameter. We introduce a fixed-point theory that allows for the exhaustive synthesis of all the valuations of the variables which make the pmARTCL formulae hold in a given model. The theory has been implemented in an open source stand-alone tool and evaluated on scalable examples with promising results. |
|
|