LACL, bâtiment P2-RdC, salle des thèses: comment y aller
Abstract: In game theory, as well as in the semantics of game logics, a strategy can be represented by any function from states of the game to the agent's actions. That makes sense from the mathematical point of view, but not necessarily in the context of human behavior. This is because humans are quite bad at executing complex plans, and also rather unlikely to come up with such plans in the first place. In this work, we adopt the view of bounded rationality, and look only at "simple" strategies in specifications of agent's abilities. We formally define what "simple" means, and propose a variant of alternating-time temporal logic that takes only such strategies into account. We also study the model checking problem for the resulting semantics of ability.
Abstract: Self modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, especially in malware to make the code hard to analyse and to detect by anti-viruses. Thus, the analysis of such self modifying programs is a big challenge. Pushdown systems (PDSs) is a natural model that is extensively used for the analysis of sequential programs because they allow to accurately model procedure calls and mimic the program's stack. In this work, we propose to extend the PushDown System model with self modifying rules. We call the new model Self-Modifying Push-Down System (SMPDS). A SM-PDS is a PDS that can modify its own set of transitions during execution. We show how SMPDSs can be used to naturally represent self-modifying programs and provide efficient algorithms to compute the backward and forward reachable configurations of SMPDSs. We implemented our techniques in a tool and obtained encouraging results. In particular, we successfully applied our tool for the detection of self-modifying malware. This is a joint work with Tayssir Touili.