29 Juin - 5 Juillet


Retour à la vue des calendrier
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.