|
![](images/spacer.gif) |
Mardi 10 Janvier
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Algorithmes efficaces de génération aléatoire contrainte |
Description: |
Philippe Duchon |
Heure: |
15:00 - 18:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Combinatorial physics, hypergeometric functions and symmetries of differential equations |
Description: |
Youssef Abelaziz |
Jeudi 12 Janvier
Heure: |
13:00 - 14:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Harnessing Malware Intelligence for Defense and Attribution |
Description: |
Arun Lakhotia The number of unique malware has been doubling every year for over two decades. The majority of effort in malware analysis has focused on methods for preventing malware infection. We view the exponential growth of malware as an underutilized source of intelligence. Given that the number of malware authors are not doubling each year, the large volume of malware must contain evidence that connects them. The challenge is how to extract the connections and do so in a timely manner to be useful.
This talk will describe Cythereal MAGIC, a cloud-based malware analysis service, for mining large scale malware repositories. MAGIC, an offshoot of research conducted under the DARPA Cyber Genome program, uses malware "genome" to construct features that are resilient to many obfuscations. The correlations discovered by MAGIC can be used to prevent and detect zero-day malware. The correlations can also be used to investigate malware attacks for attribution. |
Heure: |
15:30 - 16:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Parametric model checking timed automata under non-Zenoness assumption |
Description: |
Gia Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions in a finite time), which is unrealistic. On the one hand, we show that synthesizing parameter valuations such that at least one counter-example run is non-Zeno is undecidable for Parametric Timed Automata (PTA). On the other hand, we propose a procedure based on a transformation of PTA into Clock Upper Bound PTA to derive such valuations. |
|
|