Tayssir Touili

Xin Ye

SMODIC: A Model Checker for Self-modifying Code

Keywords: Malware detection, Pushdown Systems, Model Checking ACM Reference Format:

In this paper, we present SMODIC, a model checker for selfmodifying binary codes. SMODIC uses Self Modifying Pushdown Systems (SM-PDS) to model self-modifying binary code. This allows to faithfully represent the program's stack as well as the self-modifying instructions of the program. SMODIC takes a selfmodifying binary code or a self modifying pushdown system as input. It can then perform reachability analysis and LTL/CTL modelchecking for these models. We successfully used SMODIC to modelcheck more than 900 self-modifying binary codes. In particular, we applied SMODIC for malware detection, since malwares usually use self-modifying instructions, and since malicious behaviors can be described by LTL or CTL formulas. In our experiments, SMODIC was able to detect 895 malwares and to prove that 200 benign programs were benign. SMODIC was also able to detect several malwares that well-known antiviruses such as Bit-Defender, Kinsoft, Avira, eScan, Kaspersky, Baidu, Avast, and Symantec failed to detect. SMODIC can be found in https://lipn.univ-paris13.fr/~touili/smodic

CCS CONCEPTS

• Theory of computation → Verification by model checking;

• Security and privacy → Logic and verification.

INTRODUCTION

Self-modifying code is code that modifies its own instructions while it is executing. It has been used for a long time to hide the internals of a program. It was e.g. applied to reverse engineering for protection [START_REF] Madou | Software protection through dynamic code mutation[END_REF], since hiding the codes of a program can protect some intellectual property contained by software. Recently, it has also been widely used by malware writers to hide their malicious intent and evade from anti-virus detection. As malwares have become a big security threat to our daily life, malware detection is a critical problem in both industry and academic areas. Thus, being able to analyse self-modifying code is becoming of the utmost importance, since it is widely used by malwares.

There are several kinds of possibilities to make a binary code selfmodifying. One of these techniques is packing and unpacking. Such techniques were extensively studied e.g. in [START_REF] Bergeron | Static detection of malicious code in executable programs[END_REF][START_REF] Bonfante | A construction of a self-modifiying language with a formal correction proof[END_REF][START_REF] Christodorescu | Semantics-aware malware detection[END_REF][START_REF] Balakrishnan | Model Checking x86 Executables with CodeSurfer/x86 and WPDS++[END_REF][START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Singh | Static verification of worm and virus behavior in binary executables using model checking[END_REF]. In this work, we consider self-modifying code implemented by self-modifying instructions, which are instructions that consider code as data. This allows them to read and write into code, thus producing self-modifying instructions. Such instructions are usually mov instructions, since they allow to read and write into memory. To illustrate this, let us consider the code of Figure 1. This is a segment of the worm Worm.Whboy equipped with a selfmodifying instruction. The goal of this worm is to spread itself and infect computers through file downloading. The first step for Worm.Whboy to infect a host is to make a copy of itself into it. For this, it needs to call the API function GetSystemDirectoryA (address 0x13) to get its location, and then the API functions LStrCatN and CheckPath (addresses 0x2a and 0x35) to check the path. Let us now show how self-modifying code can fool a static analyser and can make this malware undetectable by an antivirus. In Figure 1, the box on the left gives, respectively, the binary code, the corresponding addresses of the different instructions, and the corresponding assembly instruction at each address. For example, ff is the binary code of the instruction push. Thus, the first line is translated to push 0b. The second line is translated to mov 0x2 0xc, since c6 is the binary code of the instruction mov, etc. Let us now execute this code. First, push 0b is executed, then mov 0x2 0xc. This last instruction will replace the first byte at address 0x2 by 0xc. Thus, at address 0x2, ff 0b is replaced by 0c 0b. Since 0c is the binary code of jmp, this means the instruction push 0b is replaced by jmp 0xb. Therefore, this code is self-modifying. If we model this piece of code blindly, without looking at the semantics of the different instructions, we will extract from it the Control Flow Graph CFG a of Figure 1, in which the API functions GetSystemDirectoryA, LStrCatN and CheckPath responsible of the malicious behavior cannot be reached. However, the correct Control Flow Graph of this piece of code is CFG b. Thus, if we do not take into account the fact that the instruction mov 0x2 0xc is self-modifying, then this code will be declared as benign, whereas it is malicious. Therefore, it is very important to be able to deal with self-modifying code implemented by mov instructions.

In this paper, we present SMODIC, a model checker for selfmodifying binary code that use self-modifying mov instructions. In SMODIC, such binary code is modeled using Self Modifying Pushdown Systems (SM-PDS) [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF], which is an extension of standard Pushdown Systems (PDS) that can modify its own instructions during its execution. As advocated in [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF], using SM-PDSs is suitable for this kind of self-modifying binary code as it allows to faithfully represent the program's stack as well as the self-modifying mov instructions of the program. SMODIC takes as input either a selfmodifying binary code or a self modifying pushdown system. It can then perform reachability analysis and LTL/CTL model-checking for these models. SMODIC first adapts the tool Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF] to get the Control Flow Graph from the binary code. Then, it translates this CFG into a SM-PDS. It then implements the algorithms of [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF][START_REF] Touili | LTL Model Checking for Self Modifying Code[END_REF] to perform reachability analysis and LTL/CTL model-checking for this model.

We successfully used SMODIC to model-check more than 900 self-modifying binary codes. In particular, we applied SMODIC for malware detection, since malwares usually use self-modifying instructions. Indeed, malicious behaviors can be described by LTL or CTL formulas. In our experiments, SMODIC was able to detect 895 malwares and to prove that 200 benign programs were benign. SMODIC was also able to detect several malwares that well-known antiviruses such as Bit-Defender, Kinsoft, Avira, eScan, Kaspersky, Baidu, Avast, and Symantec failed to detect. SMODIC can be found in https://lipn.univ-paris13.fr/~touili/smodic.

Outline. Section 3 introduces the theoretical background of SMODIC. Section 4 shows how can SMODIC be used for malware detection. Section 5 describes the architecture of SMODIC. The experiments are discussed in Section 6.

RELATED WORK

Model checking and static analysis approaches have been widely used to analyze binary programs, for instance, in [START_REF] Bergeron | Static detection of malicious code in executable programs[END_REF][START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Balakrishnan | Model Checking x86 Executables with CodeSurfer/x86 and WPDS++[END_REF][START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Singh | Static verification of worm and virus behavior in binary executables using model checking[END_REF]. Temporal Logics were chosen to describe malicious behaviors in [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF][START_REF] Nguyen | CARET model checking for malware detection[END_REF][START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Beaucamps | Behavior Abstraction in Malware Analysis[END_REF]. However, these works cannot deal with selfmodifying code.

There are several researches on self-modifying code. Cai et al. [START_REF] Cai | Certified self-modifying code[END_REF] use local reasoning and separation logic to describe selfmodifying code and treat program code uniformly as regular data structure. However, [START_REF] Cai | Certified self-modifying code[END_REF] requires programs to be manually annotated with invariants. In [START_REF] Debray | On the semantics of self-unpacking malware code[END_REF], the authors propose a formal semantics for self-modifying codes, and use that to represent selfunpacking code. This work only deals with packing and unpacking behaviours. Bonfante et al. [START_REF] Bonfante | A computability perspective on self-modifying programs[END_REF] provide an operational semantics for self-modifying programs and show that they can be constructively rewritten to a non-modifying program. However, all these specifications [START_REF] Bonfante | A computability perspective on self-modifying programs[END_REF][START_REF] Cai | Certified self-modifying code[END_REF][START_REF] Debray | On the semantics of self-unpacking malware code[END_REF] are too abstract to be used in practice. In [START_REF] Bertrand | A model for self-modifying code[END_REF], the authors propose a new representation of self-modifying code named State Enhanced-Control Flow Graph (SE-CFG). SE-CFG extends standard control flow graphs with a new data structure, keeping track of the possible states programs can reach, and with edges that can be conditional on the state of the target memory location. It is not easy to analyse a binary program only using its SE-CFG, especially that this representation does not allow to take into account the stack of the program. [START_REF] Blazy | Verified abstract interpretation techniques for disassembling low-level self-modifying code[END_REF] propose abstract interpretation techniques to compute an over-approximation of the set of reachable states of a self-modifying program, where for each control point of the program, an over-approximation of the memory state at this control point is provided. [START_REF] Roundy | Hybrid analysis and control of malware[END_REF] combine static and dynamic analysis techniques to analyse self-modifying programs. Unlike our approach, these techniques [START_REF] Roundy | Hybrid analysis and control of malware[END_REF][START_REF] Blazy | Verified abstract interpretation techniques for disassembling low-level self-modifying code[END_REF] cannot handle the program's stack.

Unpacking binary code is also considered in [START_REF] Debray | Reverse engineering self-modifying code: Unpacker extraction[END_REF][START_REF] Coogan | Automatic static unpacking of malware binaries[END_REF][START_REF] Gyung | Renovo: A hidden code extractor for packed executables[END_REF][START_REF] Royal | Polyunpack: Automating the hidden-code extraction of unpack-executing malware[END_REF][START_REF] Debray | On the semantics of self-unpacking malware code[END_REF]]. These works do not consider self-modifying mov instructions.

There are a lot of tools that can deal with binary code analysis [2-4, 7-9, 11, 13, 14, 22, 24-26, 37, 39, 41]. POMMADE [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF] is a malware detector based on LTL and CTL model-checking of pushdown systems. STAMAD [START_REF] Dam | Malware Detection based on Graph Classification[END_REF][START_REF] Dam | Learning Malware Using Generalized Graph Kernels[END_REF][START_REF] Dam | Precise Extraction of Malicious Behaviors[END_REF] is a malware detector based on PDSs and machine learning. However, all these tools cannot handle self-modifying code. The only tools that we know of and that can deal with self-modifying code are BE-PUM [START_REF] Nguyen | Pushdown model generation of malware[END_REF] and CoDisasm [START_REF] Bonfante | CoDisasm: medium scale concatic disassembly of self-modifying binaries with overlapping instructions[END_REF]. BE-PUM (Binary Emulation for PUshdown Model) [START_REF] Nguyen | Pushdown model generation of malware[END_REF] focuses on generating CFG (Control Flow Graph) of malwares. BE-PUM can construct a pushdown model from x86 binaries in an on-the-fly manner. Concolic testing is applied to determine the precise destinations of branches for indirect jumps. This tool can deal with self-modifying code caused by modifying the destinations of indirect jumps, including overwriting the return address of a function (in the stack). But it cannot handle self-modifying instructions. CoDisasm [START_REF] Bonfante | CoDisasm: medium scale concatic disassembly of self-modifying binaries with overlapping instructions[END_REF] is a tool that focuses on the disassembly of x86 code that includes self-modifying instructions and code overlapping. CoDisasm deals only with disassembling the code. It does not consider model-checking problems of code.

BACKGROUND 3.1 Self-modifying Pushdown Systems

A Self-modifying Pushdown System (SM-PDS) is a Pushdown System (PDS), i.e. an automaton equipped with a stack, that can dynamically modify its set of rules during the execution time: in addition to the standard push and pop transition rules of a pushdown system, a SM-PDS has self-modifying rules of the form 𝑝

(𝑟 1 ,𝑟 2 )
↩----→ 𝑝 ′ that move the SM-PDS from control point 𝑝 to control point 𝑝 ′ , while removing 𝑟 1 from the set of rules of the SM-PDS and adding 𝑟 2 to it. Thus, an SM-PDS has the capability to change its own set of transition rules during the execution. For more details about the SM-PDS model, we refer the reader to [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF].

From Self-modifying Code to SM-PDS

To translate a binary code with self-modifying mov instructions to a SM-PDS, we use the translation of [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF]. The basic idea is that the control locations of the SM-PDS store the control points of the binary program and the stack mimics the program's stack. Our translation relies on the disassembler Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF] to disassemble binary code, construct the control flow graph (CFG), determine indirect jumps, compute the possible values of the used variables, registers and the memory locations at each control point of the program. After getting the control flow graph whose edges are equipped with disassembled instructions, we translate the CFG into a SM-PDS as described in [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF]. The non self-modifying instructions of the program define the standard PDS rules of the SM-PDS and can be obtained following the translation of [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF] that models non selfmodifying instructions of the program by a PDS. Self-modifying instructions are represented using self-modifying rules. For more details, we refer the reader to [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF].

The Model Checking Algorithms

We use finite automata to finitely represent regular infinite sets of configurations of a SM-PDS. Then, the sets of predecessors and successors of a SM-PDS are computed using a kind of a saturation procedure on the finite automata [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF]. As for LTL and CTL modelchecking, they can be reduced to the emptiness problem for Selfmodifying (Alternating) Büchi Pushdown Systems. The basic idea is to make a product of the given SM-PDS and the given LTL or CTL formula to get a Self-modifying (Alternating) Büchi Pushdown system and then apply the algorithms of [START_REF] Touili | LTL Model Checking for Self Modifying Code[END_REF] to check the emptiness of the Self-modifying (Alternating) Büchi Pushdown system.

APPLYING SMODIC FOR MALWARE DETECTION

SMODIC can be used for malware detection. Indeed, as shown in [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF], malicious behaviors can be described by LTL or CTL formulas. For example, we show in this section how LTL can be used to express the malicious behavior of registry key injecting. Other LTL and CTL formulas that describe other malicious behaviors can be found in [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF][START_REF] Touili | LTL Model Checking for Self Modifying Code[END_REF].

In order to get started at boot time, many malwares add themselves into the registry key listing. This behavior is typically implemented by first calling the API function GetModuleFileNameA to retrieve the path of the malware's executable file. Then, the API function RegSetValueExA is called to add the file path into the registry key listing. As a result, the malware can execute itself automatically. This behavior can be expressed by the following LTL formula:

F 𝑐𝑎𝑙𝑙 𝐺𝑒𝑡𝑀𝑜𝑑𝑢𝑙𝑒𝐹𝑖𝑙𝑒𝑁 𝑎𝑚𝑒𝐴 ∧ F( 𝑐𝑎𝑙𝑙 𝑅𝑒𝑔𝑆𝑒𝑡𝑉 𝑎𝑙𝑢𝑒𝐸𝑥𝐴)
This formula expresses that if a call to the API function GetMod-uleFileNameA is followed by a call to the API function RegSetVal-ueExA, then probably a malware is trying to add itself into the registry key listing.

LdPinch.ch is such a malware that uses registry key injecting to execute itself. Fig. 3 shows a disassembled fragment of this malware. Note that this fragment contains self-modifying codes in address 00401547: mov replaces the value at address 0040154A with 6A (which is the binary code of push). If we abstract away the fact that this code is self-modifying, and we treat this piece of code as if it were not self-modifying (as done in most of the other tools for binary code), then we will reach the conclusion that this code is not malicious. Indeed, in this case, a loop between address 00401545 and address 0040154A will be detected and we will reach the conclusion that the API functions responsible of the malicious behavior cannot be called.

However, in reality, after the execution of mov 0040154A c6, the instruction at address 0040154A will be changed to push 00401545 and the remaining instructions will be executed: GetModuleFileNameA and RegSetValueExA will be called, and we will reach the conclusion that this code is malicious.

ARCHITECTURE

The Architecture of SMODIC is shown in Figure 2. SMODIC takes as input either a binary program or a SM-PDS. SMODIC can perform both reachability analysis and LTL/CTL model checking. If the input of SMODIC is a binary program, it is passed to the component Oracle. This component is based on the disassembler Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF]. It takes as input a binary program, and outputs its corresponding assembly program, its corresponding Control Flow Graph (CFG) equipped with the assembly instruction corresponding to each edge, together with informations about the called API functions, and the different values of the registers and memory addresses at each control point. All these outputs are fed to the component Model Builder that will compute the corresponding SM-PDS.

The Reachability component takes as input a SM-PDS, and a sequence of API functions, and applies the reachability algorithms of [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF] to check whether the SM-PDS has a run that calls these API functions in this order. For example, if we consider the sequence 𝑓 1 , 𝑓 2 , 𝑓 3 , then Reachability component checks whether the SM-PDS has a run that calls first 𝑓 1 , then 𝑓 2 , then 𝑓 3 . The LTL (CTL) component takes as input a SM-PDS and an LTL (CTL) formula, and applies the algorithms of [START_REF] Touili | LTL Model Checking for Self Modifying Code[END_REF] to check whether the SM-PDS satisfies the LTL (CTL) formula.

EXPERIMENTS

A SM-PDS can be translated into an equivalent Pushdown System (PDS) [START_REF] Touili | Reachability Analysis of Self Modifying Code[END_REF]. Thus, to perform reachability, and LTL/CTL modelchecking for an SM-PDS, one can translate it into an equivalent

Address Assembly Binary

Figure 3: A Fragment of LdPinch.ch PDS, and then apply the standard algorithms for reachability and LTL/CTL model-checking for standard PDSs [START_REF] Esparza | Efficient Algorithms for Model Checking Pushdown Systems[END_REF][START_REF] Kiefer | Moped -A Model-Checker for Pushdown Systems[END_REF][START_REF] Song | PuMoC: a CTL model-checker for sequential programs[END_REF]. We show in this section how, in our experiments, translating the SM-PDS into an equivalent PDS is not efficient and that our tool SMODIC behaves much better. We also show how our tool SMODIC can be successfuly applied for malware detection. All our experiments were run on Ubuntu 16.04 with a 2.7 GHz CPU, 2GB of memory.

SMODIC vs. standard PDS Model-checking

To compare the performance of SMODIC against the approach that consists in translating the SM-PDS into an equivalent PDS or symbolic PDS [START_REF] Esparza | Efficient Algorithms for Model Checking Pushdown Systems[END_REF][START_REF] Kiefer | Moped -A Model-Checker for Pushdown Systems[END_REF] and then apply the standard 𝑝𝑜𝑠𝑡 * , 𝑝𝑟𝑒 * , LTL and CTL algorithms for PDSs and symbolic PDSs [START_REF] Esparza | Efficient Algorithms for Model Checking Pushdown Systems[END_REF][START_REF] Kiefer | Moped -A Model-Checker for Pushdown Systems[END_REF][START_REF] Song | PuMoC: a CTL model-checker for sequential programs[END_REF], we first applied our tool on randomly generated SM-PDSs of various sizes. SMODIC was able to successfully handle all cases in only a few seconds. Then, we translated these SM-PDSs into equivalent PDSs or symbolic PDSs and run the tools MOPED [START_REF] Kiefer | Moped -A Model-Checker for Pushdown Systems[END_REF] (for reachability and LTL model checking), or PuMoC [START_REF] Song | PuMoC: a CTL model-checker for sequential programs[END_REF] (for CTL model checking). Going through PDSs or symbolic PDSs is less efficient and leads to memory out in several cases, whereas SMODIC was able to deal with all the cases in only a few seconds. The results (CPU Execution time) for the LTL component are shown in Table 1.

In Table 1, Column Size is the size of the SM-PDS (𝑆 1 for non selfmodifying transitions and 𝑆 2 for self-modifying transitions). Column LTL gives the size of the transitions of the Büchi automaton generated from the LTL formula (using the tool LTL2BA [START_REF] Gastin | Fast LTL to Büchi automata translation[END_REF]). Column SMODIC gives the cost of SMODIC. Column PDS shows the cost it takes to get the equivalent PDS from the SM-PDS. Column Result reports the cost it takes to run the LTL PDS model-checker Moped [START_REF] Kiefer | Moped -A Model-Checker for Pushdown Systems[END_REF] for the PDS we got. Column Total is the total cost it takes to translate the SM-PDS into a PDS and then apply the standard LTL model checking algorithm of Moped (Total=PDS+Result). Column Symbolic PDS reports the cost it takes to get the equivalent Symbolic PDS from the SM-PDS. Column 𝑅𝑒𝑠𝑢𝑙𝑡 1 is the cost to run the Symbolic PDS LTL model-checker Moped. Column 𝑇𝑜𝑡𝑎𝑙 1 is the total cost it takes to translate the SM-PDS into a symbolic PDS and then apply the standard LTL model checking algorithm of Moped. You can see that SMODIC (Column SMODIC) is much more efficient than translating the SM-PDS to an equivalent (symbolic) PDS, and then run the standard LTL model-checker Moped. Translating the SM-PDS to a standard PDS may take more than 20 days, whereas our tool SMODIC takes only a few seconds. Moreover, since the obtained standard (symbolic) PDS is huge, Moped failed to handle several cases (the time limit that we set for Moped is 20 minutes), whereas SMODIC was able to deal with all the cases in only a few seconds.

Detecting Real Malwares

We applied SMODIC to detect several malwares. We consider 895 malwares from VX heaven [START_REF] Heaven | [END_REF], VirusShare [START_REF] Virusshare | vXshare[END_REF], and MalShare [START_REF] Cutler | malshare[END_REF]. We also choose 200 benign samples from Windows XP system (win32). We consider self-modifying versions of the malwares. In these versions, the malicious behaviors are unreachable if the semantics of the self-modifying instructions are not taken into account, i.e., if the self-modifying instructions are considered as "standard" instructions that do not modify the code, then the malicious behaviors cannot be reached. First, we abstract away the semantics of the self-modifying instructions and model such programs as standard PDSs (as in [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF] 2: SMODIC vs. well known anti-viruses model-checking for PDSs to determine whether the programs contain any malicious behavior. In this case, none of the programs was declared as malicious. Then, we use SM-PDSs to model these programs, thus, taking self-modifying instructions into consideration: we use SMODIC to model these programs using SM-PDSs and to check whether these SM-PDSs satisfy any malicious LTL/CTL formula in our database. SMODIC was able to detect all malwares, and to calssify benign programs as benign.

Comparison with well-known antiviruses.

We also compare our tool against well-known and widely used antiviruses. In order to have a fair comparision, we need to consider new malwares, since anti-viruses know the signatures of all the known malwares. Thus, the challenge for anti-viruses is to detect new malwares. To this aim, we use the sophisticated malware generator NGVCK available at VX Heavens [START_REF] Heaven | [END_REF] to generate 200 new malwares. Then we obfuscate these malwares with self-modifying code. Then, we feed these malwares to SMODIC and to well-known antiviruses such as BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Baidu, Avast, and Symantec to detect them. Our tool was able to detect all these programs as malicious, whereas none of the well-known antiviruses was able to detect all these malwares. Table 2 reports the detection rates of our tool and the well-known anti-viruses.

Figure 1 :

 1 Figure 1: An Example of Self-modifying code

  ), and perform LTL/CTL SMODIC McAfee Norman BitDefender Kinsoft Avira eScan Kaspersky Qihoo360 Avast Symantec

	100%	27.6%	22.1%	33.1%	14.4% 28.3% 21.4%	56.2 %	35.9%	50.7%	77.9%
				Table

Size


Tayssir Touili

Register Automata for Malware Specification

Keywords: Malware detection, Model-checking, Automata, Pushdown Systems Tayssir Touili. 2018. Register Automata for Malware Specification. In ARES2022. ACM, New York, NY

With the huge impact that internet is having in our daily life, it is becoming urgent to have efficient malware detection techniques. In this paper, we present a new approach to perform malware detection. We use register automata to describe malware specifications, and pushdown systems to model the program. This allows to keep track of both the program's stack and the values of the registers. Indeed, both the stack and the registers are needed to have precise malware specifications. To check whether the program contains some malicious behavior, we perform a kind of product between the pushdown system and the register automaton describing the malicious behaviors. Whether the program is malicious or not is then reduced to reachability checking in pushdown systems. We implemented our techniques in a prototype and obtained encouraging preliminary results.

Introduction

Internet is taking more and more place in our daily life as it offers a huge number of services. Unfortunately, the internet can also be a source of threat to your computer or smart phone, as it vehiculates an enormeous number of malwares. Malwares can be very dangerous, for example, authorities investigating the 2008 crash of Spanair flight 5022 have discovered a central computer system used to monitor technical problems in the aircraft was infected with malware. Thus, it is crucial to have efficient up-to-date malware detectors. There are mainly two existing approaches for malware detection: signature scanning and code emulation. An antivirus based on signature scanning compares the content of a file with the entries of a dictionary that has the signatures of known viruses. If it finds a match, it is almost certain that the file is actually infected. The main disadvantages of such techniques are that it is possible for a user to be infected with a new virus for which there is not an existing signature, the signature dictionary must be kept up to date, and if some of the virus instructions change (even if it doesn't change its behaviour) its signature becomes obsolete. As for code emulation techniques, they will simulate the suspicious file and try to detect any malicious behavior. The main disadvantage of such techniques is that they cannot simulate the code indefinitely. If the malicious behavior shows itself quickly, it will be detected, but if it has to wait for a particular date, or the execution of an event, etc., the waiting could be too long and the emulation would have to terminate without detecting the malware. Thus, an efficient malware detector should try to detect the malware without executing the program, and should be more evolved than searching for syntactic signatures. It has to analyse the behavior of the program without executing it. Therefore, model-checking is a good candidate to perform malware detection as it allows to analyse the behaviors of a program without executing it.

Model-checking and static analysis techniques have been applied to detect malicious behaviors e.g. in [2-7, 9, 10, 12-15, 18]. However, all these works are based on modeling the program as a finite-state system, and thus they cannot accurately model the program's stack. Being able to track the program's stack is very important for malware detection as explained in [START_REF] Lakhotia | A Method for Detecting Obfuscated Calls in Malicious Binaries[END_REF]. For example, malware writers obfuscate the system calls by using pushes and jumps to make malware hard to analyze, because anti-viruses usually determine malware by checking function calls to operating systems.

To overcome this problem, [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Song | Pushdown Model Checking for Malware Detection[END_REF][START_REF] Song | LTL Model-Checking for Malware Detection[END_REF][START_REF] Song | PoMMaDe: pushdown modelchecking for malware detection[END_REF] proposed to use pushdown systems as program model when performing malware detection. However, these works don't involve the values of the registers of the program in the malware specifications. In several cases, the values of some registers are needed to determine whether some behavior is malicious or not. For example, several Windows viruses search for a file with a .EXE extension (a file ready to get executed), and overwrites the content of this file with their own code. To search for a file, the virus will typically call the interruption 21h with the value 4eh in the register ah, the searched file's attributs in the register cl, and a pointer to the path or the name of the searched file in dx. To write to a file, the virus will typically call the interruption 21h with a file handle in bx, the number of bytes to write in cx, and a pointer to the buffer that has the data to be written in dx. Another example of a Windows' virus behavior is the interruption hook, where the virus tries to fool DOS by making it think that it is calling an interruption whereas it is actually calling the virus. To do this, the virus will typically put a pointer to itself in the memory address where one should usually find a pointer to a particular interruption. One of the interruptions that can be hooked is 13h as it allows to write data to the boot sector of a disk. To this aim, this interruption need to be called with the value 301h set in ax, and 1 in cl to write the data pointed by bx to the boot sector of the disk defined by the value in dx. Thus, to check whether a program that calls these interruptions is a virus or not, it is crucial to know the values of the corresponding registers.

Therefore, keeping track of the values of the registers is important to accurately describe malware behaviors. Hence, we propose in this paper to use register automata to describe malware specifications, and to use pushdown systems to model the program. This allows to keep track of both the program's stack and the values of the registers. To check whether the program contains some malicious behavior, we perform a kind of product between the pushdown system and the register automaton describing the malicious behaviors. Whether the program is malicious or not is then reduced to reachability checking in pushdown systems. We implemented our techniques in a prototype and obtained encouraging preliminary results.

Outline. This paper is organized as follows. In the next section, we define register automata and show how they can be used to precisely specify malwares. Section 3 describes the translation from a binary code to a pushdown system, as malwares are executables and hence, are binary programs. Section 4 shows how malware detection is reduced to reachability checking in pushdown systems. We conclude the paper with a conclusion and a description of future work.

Malicious behavior specification

In this section, we introduce register automata and show how they can be used to specify malicious behaviors.

Register automata

Definition 2.1 (Registers). Let R = {𝑟 1 , ..., 𝑟 𝑛 } be a set of registers (here R is the set of registers used by the assembly program). An instantiation R of R is defined by: 𝑅 In what follows, if there is no confusion, we will write

= {|𝑟 1 | = 𝑣𝑎𝑙 1 , ..., |𝑟 𝑛 | = 𝑣𝑎𝑙 𝑛 },
𝑟 𝑖 = 𝑣𝑎𝑙 𝑖 instead of |𝑟 𝑖 | = 𝑣𝑎𝑙 𝑖 .
To specify malicious behaviors, we will introduce register automata. Such an automaton can be seen as an ordinary finite-state automaton augmented with registers over a finite domain. A state of such an automaton consists of a control location and a register valuation.

Definition 2.2 (Register Automaton). A register automaton is a tuple

𝐴 = ⟨𝐼𝑛𝑠𝑡, R, 𝑄, Δ, 𝑞 0 , 𝑞 𝑓 ⟩, where • 𝐼𝑛𝑠𝑡 is the set of valid instructions of the used assembly language, • R is a finite set of registers, • 𝑄 is a finite set of states, • Δ = Δ 0 ∪ Δ 1 is a finite set of transitions, where
-Δ 0 is a set of transitions of the form (𝑞, 𝑖𝑛𝑠𝑡, 𝑞), for every 𝑞 ∈ 𝑄, and every 𝑖𝑛𝑠𝑡 ∈ 𝐼𝑛𝑠𝑡. -Δ 1 is a set of transitions of the form (𝑞, 𝑖𝑛𝑠𝑡, 𝑔, 𝑞 ′ ),

where 𝑞, 𝑞 ′ ∈ 𝑄, 𝑖𝑛𝑠𝑡 ∈ 𝐼𝑛𝑠𝑡 and 𝑔 is a constraint over R.

• 𝑞 0 is the initial state, • 𝑞 𝑓 is the final state.
Intuitively, the malicious specifications are described by the transitions of Δ 1 . The transitions Δ 0 can be seen as star transitions that allow to read the transitions of the program of the analysed file that do not correspond to the malicious pattern, i.e., that are not typical for a malware. For every transition of Δ 1 , 𝑔 is a constraint that will represent the content of certain registers during the execution of the instruction 𝑖𝑛𝑠𝑡. A transition of the form (𝑞, 𝑖𝑛𝑠𝑡, 𝑔, 𝑞 ′ ) can be fired only if the current instantiation of the registers at state 𝑞 satisfies the contraint 𝑔.

Modeling malicious behaviors using register automata

In this section, we show on some examples of Windows viruses how register automata can be used to precisely describe malicious behaviors. We fix in this section R to be the set of the registers used by the considered programs: R = {ax, bx, cx, dx, ah, al, dh, dl, cs, ds, es, ss, sp, bp, si, di}.

2.2.1

File infection after a file search. Several viruses will search the files they want to infect. To do this, they will call the interruption 21h with value 4eh in the register ah, and a pointer to the extension of the searched file name (for example "*.com", "*.exe", etc) in the register dx. Once the file is found, the virus will copy itself into it. To do this, the virus will make another call to int 21h with value 40h in ah, the number of bytes to be written in cl and the location of the first byte to be written in dx. Table 1 gives a fragment of the disassembled code of the virus Intruder-B, where . . . represent pieces of code that are not interesting for the specification of the virus. You can see that this virus meets the above description.

The above specification can be described by the register automaton 𝐴 1 depicted in Figure 1. In this figure, the transitions of Δ 0 are represented by loops labelled by * . 𝐴 1 has 𝑄 = {𝐼𝑛𝑖𝑡, 𝑆1, 𝐴𝑙𝑎𝑟𝑚𝑒} as set of states, where 𝐼𝑛𝑖𝑡 is the initial state, and 𝐴𝑙𝑎𝑟𝑚𝑒 is the final state. Its set of transitions Δ 1 is the following: In Figure 1, for presentation matters, if the constraint 𝑔 is {𝑎ℎ = 4𝑒ℎ, 𝑑𝑥 = " * .𝑒𝑥𝑒"}, for example, we will write: 𝑅𝑒𝑔 = {𝑎ℎ = 4𝑒ℎ, 𝑑𝑥 = " * .𝑒𝑥𝑒"}, just to remind that these are constraints on the values of the registers.

• (𝐼𝑛𝑖𝑡, int 21h, 𝑎ℎ = 4𝑒ℎ 𝑑𝑥 = " * .𝑐𝑜𝑚" , 𝑆1

File infection without file search.

A virus could hook the file opening routine. In this case, when a program tries to open a file, it will pass the control to the virus instead of passing it to the opening routine, and the registers will have all the needed values for the correct execution of the opening routine. So the virus will get for free the name of the file we are trying to open. The viral behavior in this type of virus is to see if the file has the searched extension (".com" or ".exe"). If so, the virus will copy itself into the file. To do this, it will make a call to int 21h with value 40h in ah, the number of bytes to be written in cl and the location of the first byte to be written in dx. This behavior is present, for example, in the virus Sequin. Table 2 shows a fragment of this virus which corresponds to the behavior described above.

The above specification can be described by the register automaton 𝐴 2 depicted in Figure 2. 𝐴 2 has 𝑄 = {𝐼𝑛𝑖𝑡, 𝑆1, 𝑆2, 𝑆3, 𝑆4, 𝐴𝑙𝑎𝑟𝑚𝑒} as set of states, where 𝐼𝑛𝑖𝑡 is the initial state, and 𝐴𝑙𝑎𝑟𝑚𝑒 is the final state. Its set of transitions Δ 1 is the following, for every r ∈ R: (here ∅ means that there is no constraint to be satisfied by the registers to fire the transitions.)

• (𝐼𝑛𝑖𝑡, cmp r, '.', ∅, 𝑆1): The virus compares the value of a register with the char '. '. • (𝑆1, cmp r, 'oc', ∅, 𝑆2): The virus compares the value of a register with the string 'oc', this predicts that the virus is checking whether a file has the extension .com . • (𝑆2, cmp r, 'm', ∅, 𝑆4). The virus completes the comparison of the file extension with ".com". • (𝑆1, cmp r, 'xe', ∅, 𝑆3). The virus compares the value of a register with the string 'xe', this predicts that the virus is checking whether a file has the extension .exe. • (𝑆3, cmp r, 'e', ∅, 𝑆4). The virus completes the comparison of the file extension with ".exe".

• (𝑆4, int 21h, 𝑎ℎ = 40ℎ 𝑑𝑥 = 𝑝𝑜𝑖𝑛𝑡𝑒𝑢𝑟 _𝑣𝑖𝑟𝑢𝑠 , 𝐴𝑙𝑎𝑟𝑚𝑒). The virus will write to a file a part of its code. in ax, a pointer to the first byte to be copied in bx, the value 1 in cx and 0, 1 or 80h in dx, depending on whether the virus wants to copy itself to the boot sector of drive A, B, or to the hard disk.

The virus Boot sector virus presents this behavior. Table 3 gives a fragment of this virus that corresponds to this behavior.

The above specification can be described by the register automaton 𝐴 3 depicted in Figure 3. 𝐴 3 has 𝑄 = {𝐼𝑛𝑖𝑡, 𝐴𝑙𝑎𝑟𝑚𝑒} as set of states, where 𝐼𝑛𝑖𝑡 is the initial state, and 𝐴𝑙𝑎𝑟𝑚𝑒 is the final state. Its set of transitions Δ 1 is the folowing:

• (𝐼𝑛𝑖𝑡, int 13h,         𝑎𝑥 = 0301ℎ 𝑏𝑥 = 𝑝𝑜𝑖𝑛𝑡𝑒𝑢𝑟 _𝑣𝑖𝑟𝑢𝑠 𝑐𝑥 = 1 𝑑𝑥 = 0        
, 𝐴𝑙𝑎𝑟𝑚𝑒): The virus wants to write to the boot sector of the drive 0.

• (𝐼𝑛𝑖𝑡, int 13h,

        𝑎𝑥 = 0301ℎ 𝑏𝑥 = 𝑝𝑜𝑖𝑛𝑡𝑒𝑢𝑟 _𝑣𝑖𝑟𝑢𝑠 𝑐𝑥 = 1 𝑑𝑥 = 1        
, 𝐴𝑙𝑎𝑟𝑚𝑒): The virus wants to write to the boot sector of the drive 1.

• (𝐼𝑛𝑖𝑡, int 13h,

        𝑎𝑥 = 0301ℎ 𝑏𝑥 = 𝑝𝑜𝑖𝑛𝑡𝑒𝑢𝑟 _𝑣𝑖𝑟𝑢𝑠 𝑐𝑥 = 1 𝑑𝑥 = 0080ℎ        
, 𝐴𝑙𝑎𝑟𝑚𝑒): The virus wants to write to the boot sector of the hard disk.

                                  
              
write virus to the boot sector of drive 1 . . .

Binary Code Modeling

In this section, we show how to build a pushdown system (PDS) from a binary program. Indeed, malwares are usually executables, i.e., binary programs. We suppose we are given an oracle O that extracts from the binary program a control flow graph equipped with informations about the values of the registers and the memory locations at each control point of the program. Jakstab [START_REF] Kinder | Jakstab: A Static Analysis Platform for Binaries[END_REF] and IDA Pro [START_REF]Disassembler[END_REF] can be used to get this oracle. We translate the control flow graph into a pushdown system where the control locations store the control points of the binary program and the stack tracks the stack of the program. This translation takes into account the values of the different registers and memory locations of the program.

Control Flow Graphs

Let R be the finite set of registers used in the binary program. Let 𝑉 𝑎𝑙 be the set of possible values that can be assigned to these registers according to our modeling. 𝑉 𝑎𝑙 = [0000ℎ, 𝑓 𝑓 𝑓 𝑓 ℎ] ∪{⊥}∪{pointeur_virus}, where ⊥ is used to indicate "unknown value", and as mentionned previously, pointeur_virus is used to indicate that the register has a pointer to the program's (virus') own code. Let States be the set of functions from R ∪ [0000ℎ, 𝑓 𝑓 𝑓 𝑓 ℎ] to 2 𝑉 𝑎𝑙 . Intuitively, let 𝑠 ∈ States. For every 𝑟 ∈ R, 𝑠 (𝑟 ) gives the possible values of the register 𝑟 in the state 𝑠, while for every 𝑑 ∈ [0000ℎ, 𝑓 𝑓 𝑓 𝑓 ℎ], 𝑠 (𝑑) gives the possible values of the memory at address 𝑑 in the state 𝑠. Let EXP be the set of expressions over the registers and the memory locations used in the program. States is extended over expressions in EXP in the usual way.

A control flow graph (CFG) is a tuple 𝐺 = (𝑁 , 𝐼𝑛𝑠𝑡, 𝐸), where 𝑁 is a finite set of nodes corresponding to the control points of the program, 𝐼𝑛𝑠𝑡 is a finite set of assembly instructions used in the program, and 𝐸 : 𝑁 × 𝐼𝑛𝑠𝑡 × 𝑁 is a finite set of edges each of them associated with an assembly instruction of the program. We write 𝑛 1 𝑖 -→ 𝑛 2 for every (𝑛 1 , 𝑖, 𝑛 2 ) in 𝐸. Given a binary program, the oracle O computes a corresponding control flow graph 𝐺 and a function 𝜚 : 𝑁 -→ States that associates to each node 𝑛 an overapproximation of the set of possible states of the program at the control point 𝑛. For technical reasons, if the instruction 𝑖 at control point 𝑛 is of the form (𝑖 = mov 𝑟 , offset EXPRESSION) or (𝑖 = mov 𝑟 , [EXPRESSION]), for a register 𝑟 in R, then we let 𝜚 (𝑛) (𝑟 ) = {pointeur_virus}. Here, the program wants to put in the register 𝑟 a pointer to its own code. Therefore, we will put pointeur_virus in this register in order to say that it has a pointer to the virus code. This is important to know for virus detection as explained in the previous section. Let 𝑒𝑥𝑝 be an expression and let 𝑟 be a register involved in this expression. If 𝜚 (𝑛) (𝑟 ) = {pointeur_virus}, then 𝜚 (𝑛) (𝑒𝑥𝑝) = {pointeur_virus}.

Pushdown Systems

A Pushdown System (PDS) is a tuple P = (𝑃, Γ, 𝐴𝑐𝑡, Δ), where 𝑃 is a finite set of control locations, Γ is the stack alphabet, 𝐴𝑐𝑡 is a finite set of actions, Δ ⊆ (𝑃 × Γ) × 𝐴𝑐𝑡 × (𝑃 × Γ * ) is a finite set of transition rules.

A configuration ⟨𝑝, 𝜔⟩ of P is an element of 𝑃 × Γ * . We write ⟨𝑝, 𝛾⟩ 𝑎 ↩-→ ⟨𝑞, 𝜔⟩ instead of ((𝑝, 𝛾), 𝑎, (𝑞, 𝜔)) ∈ Δ. The successor relation ; P ⊆ (𝑃 × Γ * ) × (𝑃 × Γ * ) is defined as follows: if ⟨𝑝, 𝛾⟩ 𝑎 ↩-→ ⟨𝑞, 𝜔⟩, then ⟨𝑝, 𝛾𝜔 ′ ⟩ ; P ⟨𝑞, 𝜔𝜔 ′ ⟩ for every 𝜔 ′ ∈ Γ * . The reachability relation =⇒ P ⊆ (𝑃 × Γ * ) × (𝑃 × Γ * ) is the reflexive and transitive closure of the successor relation ; P . Formally =⇒ P is defined as follows: (1)

𝑐 =⇒ P 𝑐 for every 𝑐 ∈ 𝑃 × Γ * , (2) if ⟨𝑝, 𝛾⟩ 𝑎 ↩-→ ⟨𝑞, 𝜔⟩, then ⟨𝑝, 𝛾𝜔 ′ ⟩ =⇒ P ⟨𝑞, 𝜔𝜔 ′ ⟩ for every 𝜔 ′ ∈ Γ * , (3) if 𝑐 =⇒ P 𝑐 ′′
and 𝑐 ′′ =⇒ P 𝑐 ′ , then 𝑐 =⇒ P 𝑐 ′ .

From Control Flow Graphs to Pushdown Systems

To compute a PDS from the binary program, we follow the translation given in [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF]. The only difference with the translation of [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF] is that here we use pointeur_virus to express that the register has a pointer to the program's own code, whereas in [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF], an overapproximation of the set of addresses that the register is pointing to, computed by the oracle, is considered. Consider a binary program. Let (𝑁 , 𝐼𝑛𝑠𝑡, 𝐸) be the CFG and 𝜚 be the state function provided by the oracle O. We construct the PDS P = (𝑃, Γ, 𝐼𝑛𝑠𝑡, Δ) as follows:

• the control locations 𝑃 are the nodes 𝑁 ; • Γ is the smallest set of symbols satisfying the following: ------→ 𝑛 2 where cjmp denotes a conditional jump instruction (𝑗𝑒, 𝑗𝑔, etc.). Let flag be the flag register (ZF,CF, etc.) of cjmp. Depending on whether the flag register satisfies the condition of cjmp or not (i.e., whether 𝑓 𝑎𝑙𝑠𝑒 ∈ 𝜚 (𝑛 1 )(𝑓 𝑙𝑎𝑔) or not), we add the transition rules 𝑟 1 = ⟨𝑛 1 , 𝛾⟩

-if 𝑛 𝑐𝑎𝑙𝑙 𝑝𝑟𝑜𝑐 --------→ 𝑛 ′ ∈ 𝐸, then {𝑛 ′ } ∈ Γ where 𝑛 ′ is the return address of the call; -if 𝑛 𝑝𝑢𝑠ℎ 𝑒𝑥𝑝 --------→ 𝑛 ′ ∈ 𝐸,

Looking for the malicious behaviors in the program

The next step is to make the product between the pushdown system that models the program and the register automaton specifying the malicious behaviors. Let P = (𝑃, Γ, 𝐼𝑛𝑠𝑡, 𝛿) be a pushdown system modeling the program, and let 𝐴 = ⟨𝐼𝑛𝑠𝑡, R, 𝑄, Δ, 𝐼𝑛𝑖𝑡, 𝐴𝑙𝑎𝑟𝑚𝑒⟩ be a register automaton representing some malicious behavior, where R = {𝑟 1 , . . . , 𝑟 𝑛 } is the set of registers of the considered program, Δ = Δ 0 ∪ Δ 1 is the set of transitions as described in Definition 2.2. 𝐼𝑛𝑖𝑡 is the initial state of 𝐴 and 𝐴𝑙𝑎𝑟𝑚𝑒 is its final state. The product between 𝐴 and P is defined as the pushdown system RP = (𝑃 ′ , Γ ′ , 𝐼𝑛𝑠𝑡, 𝛿 ′ ) where:

• 𝑃 ′ = 𝑃 × 𝑄, • Γ ′ = Γ,
• 𝛿 ′ is the set of transitions defined as follows:

- Then, to check whether the program contains the considered malicious behaviors or not, we check whether the above PDS RP reaches a configuration of the form ⟨(𝑝, 𝐴𝑙𝑎𝑟𝑚𝑒), 𝜔⟩ from the initial configuration ⟨(𝑒 0 , 𝐼𝑛𝑖𝑡), 𝜖⟩, where 𝑒 0 is the entry point of the program, 𝐼𝑛𝑖𝑡 and 𝐴𝑙𝑎𝑟𝑚𝑒 are respectively the initial and final states of the register automaton describing the malicious behavior, 𝑝 ∈ 𝑃 and 𝜔 ∈ Γ * . Indeed, the paths of the above product RP that reach a control point of the form (𝑝, 𝐴𝑙𝑎𝑟𝑚𝑒) correspond to paths of the program that satisfy the malicious behaviors of the register automaton 𝐴.

If ⟨𝑝, 𝛾⟩ 𝑖𝑛𝑠𝑡 ↩-→ ⟨𝑝 ′ , 𝜔⟩ ∈ 𝛿 and (𝑠, 𝑖𝑛𝑠𝑡, 𝑠) ∈ Δ 0 , then ⟨(𝑝, 𝑠), 𝛾⟩ 𝑖𝑛𝑠𝑡 ↩-→ ⟨(𝑝 ′ , 𝑠), 𝜔⟩ ∈ 𝛿 ′ . -If ⟨𝑝, 𝛾⟩ 𝑖𝑛𝑠𝑡 ↩-→ ⟨𝑝 ′ , 𝜔⟩ ∈ 𝛿 and (𝑠, 𝑖𝑛𝑠𝑡, 𝑔, 𝑠 ′ ) ∈ Δ 1 . Let 𝐺 be the valuation 𝐺 = {|𝑟 𝑖 | = 𝜚 (𝑝) (𝑟 𝑖 ), 1 ≤ 𝑖 ≤ 𝑛}. If 𝐺 |= 𝑔, then 𝛿 ′
Thus, formally, we need to check whether ⟨(𝑒 0 , 𝐼𝑛𝑖𝑡), 𝜖⟩ =⇒ R P ⟨(𝑝, 𝐴𝑙𝑎𝑟𝑚𝑒), 𝜔⟩. This query can be answered by the standard reachability analysis algorithms for pushdown systems [START_REF] Bouajjani | Reachability Analysis of Pushdown Automata: Application to Model Checking[END_REF][START_REF] Esparza | A BDD-Based Model Checker for Recursive Programs[END_REF].

Conclusion and future work

In this work, we showed how to perform precise malware detection by keeping track of the registers of the program. We reduced the malware detection problem to reachability checking in pushdown systems. We implemented our techniques and obtained encouraging preliminary results.

As future work, we plan to improve the malicious behavior specification formalism. Indeed, register automata allow to take into account the registers' values in the malware specifications. However, they do not allow to consider constraints on the program's stack. We plan to define malware specification formalisms that allow to consider both the stack and the registers' values. For example, [START_REF] Song | Efficient Malware Detection Using Model-Checking[END_REF][START_REF] Song | Pushdown Model Checking for Malware Detection[END_REF][START_REF] Song | LTL Model-Checking for Malware Detection[END_REF][START_REF] Song | PoMMaDe: pushdown modelchecking for malware detection[END_REF] introduce the logics SLTPL and SCTPL and show how they can be used to describe the malicious behaviors while taking into account the stack. These logics extend, respectively, standard LTL and CTL with variables, quantifiers, and predicates over the stack. It would be interesting to see whether these logics could be extended with registers. This would allow to have more precise malware specifications that could deal with both the program's stack and the registers' values.

  ): This transition corresponds to a search for a file with the extension .com. • (𝐼𝑛𝑖𝑡, int 21h, 𝑎ℎ = 4𝑒ℎ 𝑑𝑥 = " * .𝑒𝑥𝑒" , 𝑆1): This transition corresponds to a search for a file with the extension .exe. • (𝑆1, int 21h, 𝑎ℎ = 40ℎ 𝑑𝑥 = 𝑝𝑜𝑖𝑛𝑡𝑒𝑢𝑟 _𝑣𝑖𝑟𝑢𝑠 , 𝐴𝑙𝑎𝑟𝑚𝑒): The virus will write a part of its code to a file. pointeur_virus is an abstraction used to indicate that the register has a pointer to the program's (virus') own code.

Figure 2 :

 2 Figure 2: File infection without file search specification

Figure 1 :

 1 Figure 1: File infection with file search specification

Figure 3 :

 3 Figure 3: Boot sector infection specification

  where 𝑒𝑥𝑝 is an expression in 𝐸𝑋 𝑃, then 𝜚 (𝑛) (𝑒𝑥𝑝) ∈ Γ where 𝜚 (𝑛) (𝑒𝑥𝑝) denotes the set of possible values of the expression 𝑒𝑥𝑝 at the control point 𝑛;• the set of rules Δ contain transition rules that mimic the instructions of the program: for every edge 𝑒 ∈ 𝐸, 𝛾 ∈ Γ:if 𝑒 = 𝑛 1 𝑝𝑢𝑠ℎ 𝑒𝑥𝑝--------→ 𝑛 2 , we add the transition rule⟨𝑛 1 , 𝛾⟩ 𝑝𝑢𝑠ℎ 𝑒𝑥𝑝 ↩-→ ⟨𝑛 2 , 𝛾 ′ 𝛾⟩,where 𝛾 ′ = 𝜚 (𝑛 1 ) (𝑒𝑥𝑝). This rule moves the program's control point from 𝑛 1 to 𝑛 2 , and pushes the set of all the possible values of the expression 𝑒𝑥𝑝 at control point 𝑛 1 onto the stack;if 𝑒 = 𝑛 1 𝑐𝑎𝑙𝑙 𝑝𝑟𝑜𝑐 --------→ 𝑛 2 , we add the transition rule ⟨𝑛 1 , 𝛾⟩ 𝑐𝑎𝑙𝑙 𝑝𝑟𝑜𝑐 ↩-→ ⟨𝑝𝑟𝑜𝑐 𝑒 , {𝑛 2 }𝛾⟩, for every 𝑝𝑟𝑜𝑐 𝑒 ∈ 𝜚 (𝑛 1 ) (𝑝𝑟𝑜𝑐).This rule moves the program's control point to the entry point of the procedure 𝑝𝑟𝑜𝑐, and pushes the return address 𝑛 2 onto the stack.if 𝑒 = 𝑛 1 𝑝𝑜𝑝 𝑒𝑥𝑝 -------→ 𝑛 2 ,we add the transition rule ⟨𝑛 1 , 𝛾⟩ 𝑝𝑜𝑝 𝑒𝑥𝑝 ↩-→ ⟨𝑛 2 , 𝜖⟩ which moves the program's control point to 𝑛 2 and pops the topmost symbol from the stack; -if 𝑒 = 𝑛 1 𝑟𝑒𝑡 ---→ 𝑛 2 , we add a transition rule ⟨𝑛 1 , 𝛾⟩ 𝑟𝑒𝑡 ↩-→ ⟨𝑎𝑑𝑑𝑟, 𝜖⟩ for every 𝑎𝑑𝑑𝑟 ∈ 𝛾. This moves the program's control point to every address 𝑎𝑑𝑑𝑟 in 𝛾, and pops the topmost symbol from the stack; -if 𝑒 = 𝑛 1 𝑐 𝑗𝑚𝑝 𝑒

  contains the transition ⟨(𝑝, 𝑠), 𝛾⟩ 𝑖𝑛𝑠𝑡 ↩-→ ⟨(𝑝 ′ , 𝑠 ′ ), 𝜔⟩. Note that this transition is considered only if 𝐺 |= 𝑔, i.e., if the values of the registers at state 𝑝 satisfy the contraint 𝑔.

  where 𝑣𝑎𝑙 1 , ..., 𝑣𝑎𝑙 𝑛 ∈ [0000ℎ, 𝑓 𝑓 𝑓 𝑓 ℎ] ∪ {⊥} ∪ {pointeur_virus}. 0000ℎ, • • • , 𝑓 𝑓 𝑓 𝑓 ℎ are the possible values of the registers in the program, ⊥ is used to indicate "unknown value". We need it if we are unable to calculate accurately the value of a register, and pointeur_virus is used to indicate that the register has a pointer to the program's (virus') own code (as will be seen later, this information is crucial for virus detection). The value 𝑣𝑎𝑙 𝑖 of the register 𝑟 𝑖 in 𝑅 will be denoted by |𝑟 𝑖 | 𝑅 .A constraint g over R is defined by 𝑔 = {|𝑟 𝑖 1 | = 𝑣𝑎𝑙 1 , ..., |𝑟 𝑖 𝑘 | = 𝑣𝑎𝑙 𝑘 }, for {𝑖 1 , ..., 𝑖 𝑘 } indices of {1, ..., 𝑛}. For every 𝑖 𝑗 ∈ {𝑖 1 , ..., 𝑖 𝑘 }, we say that 𝑟 𝑖 𝑗 is constrained by 𝑔. Let 𝑅 be an instantiation of R. We say that 𝑅 |= 𝑔 iff ∀𝑖 such that 𝑟 𝑖 is constrained by 𝑔, |𝑟 𝑖 | 𝑅 = |𝑟 𝑖 | 𝑔 . In this case, we say that the instantiation 𝑅 satisfies the constraint 𝑔.

Table 1 .

 1 Fragment of the virus Intruder-B

	. . .
	EXEFILE DB '*.EXE',0		;variable with the searched pattern
	. . .
	VIRUS:		;first code label, which is located at address 0
	. . .
	FINDEXE:
	mov dx,OFFSET EXEFILE mov cx,3FH mov ah,4EH int 21H . . .	          	search for a '*.exe' file
	INFECT:
	. . .
	mov cx,OFFSET FINAL xor dx,dx mov ah,40H int 21H . . .	          	write the virus to a file
	FINAL:
	END VIRUS

Table 2 .

 2 Fragment of the virus Sequin

	IVOFS EQU 100H	;first label of the code, wich is located at
		;address 0.
	ORG 100H
	. . .
	mov si,dx	;dx has the name of a file
	FO1:
	lodsb
	cmp al,'.'
	jne FO1
	lodsw
	or ax,2020H
	cmp ax,'oc'
	jne FEX
	lodsb
	or al,20H
	cmp al,'m'

Table 3 .

 3 Fragment of the virus Boot sector virus

	. . .
	ORG 7C00H
	. . .
	mov ax,0301H
	mov bx,7C00H
	mov cx,1
	mov dx,1
	int 13H

  ⟨𝑎𝑑𝑑𝑟, 𝛾⟩ for every 𝑎𝑑𝑑𝑟 ∈ 𝜚 (𝑛 1 ) (𝑒). 𝑟 1 moves the program's control point to 𝑛 2 whereas 𝑟 2 moves the programs's control point to the address 𝑎𝑑𝑑𝑟 that corresponds to the value of 𝑒 at point 𝑛 1 . ⟨𝑛 2 , 𝛾⟩ which moves the program's control point from 𝑛 1 to 𝑛 2 without changing the stack. Note that in this modeling, the PDS control locations correspond to the program's control points, and the PDS stack mimics the program's execution stack. The above transition rules allow the PDS to mimic the behavior of the program's stack.

	𝑐 𝑗𝑚𝑝 𝑒
	↩-→ ⟨𝑛 2 , 𝛾⟩
	𝑐 𝑗𝑚𝑝 𝑒
	and/or 𝑟 2 = ⟨𝑛 1 , 𝛾⟩ ↩-→ -if 𝑒 = 𝑛 1 𝑖 -→ 𝑛 2 is any other transition, we add a tran-
	sition rule ⟨𝑛 1 , 𝛾⟩

𝑖

↩-→


Olivier A J Martin

Jean-Dominique Gascuel

Reactive Balance Control in Immersive Visual Flows: 2D vs. 3D Virtual Stimuli

Keywords: Balance control, virtual immersion, visual flow, performance measurement, adaptation

The aim is to study the effects of 2D vs. 3D visual inputs on balance control. Ten subjects were fully immersed in virtual environment, using 10 different 2D/3D motion flow conditions. Analysis of visual and postural responses shows significant differences of reactivity in 3D versus 2D.

Introduction

The balance adaptation depends on efficient visual information processing in postural mechanisms. The visuo-postural control quickly integrates dynamic images properties to adapt motor mechanisms of balance. Our previous works have shown the ability to adapt movement and posture to visual changes [START_REF] Martin | Evaluating On-line Control of Goal Directed Arm Movement While Standing in Virtual Visual Environment[END_REF] or visuomotor discordance [START_REF] Push | HEMP -Hand-Displacement-Based Pseudo-Haptics : A study of a force field application and a behavioral analysis[END_REF] in virtual visual environments (VEs) with similar neuromotor processes as those of natural environment. However, the question about how the balance planning use visual cues is still unclear, mainly concerning the specific effects of 2D vs. 3D dynamics visual stimuli on the balance control. The goal of the study is to determine the effects of 2D vs. 3D visual inputs on ocular and balance responses. By analyzing the effects of the moving visual stimulation, this study also questions on the sensorimotor flexibility of the initial postural reaction and the online short-term balance adaptation in VEs.

Methods

Ten subjects aged from 22 to 42 participated in the study. Subjects stood within an immersive VE displayed on a 180 degrees curved screen (12x2 meters). Virtual visual stimulus consisted in randomly displayed star-like flow patterns. Ten conditions of stimuli were proposed : right, left, up and down (both in 2D and 3D), forward and backward (in 3D only). Each stimulus was presented during 20 seconds. Two randomized sessions of 10 trials per stimulus was performed, corresponding to 100 trials for each subject. A rest period occurred between sessions. Visual reactions (optokinetic nystagmus, OKN) and postural responses (kinematics and electromyography) was recorded (200Hz). Data processing and analysis focused on the visual and balance adjustments parameters; A multi-factorial statistical design was applied to data.

Results

No subject mentioned immersive discomfort or after-effect. Results show that both visual and postural motor reactive responses to virtual scene motion occurs very quickly, specifically oriented to the Direction conditions of the visual flow in both 2D and 3D (fig. 1). The automatic OKN reactions was triggered from the first scene motions. For all Direction conditions, the frequency of the ocular responses decreased for 3D flow stimulus. At postural level, rapid postural adjustments allows to maintain the head stability level.

Discussion and conclusion

The study shows measurable reactivity to both vertical and horizontal, 2D and 3D flows in VEs. Furthermore, OKN count is higher for 2D than for 3D cues. We interpret this as the result of non-uniform motion of visual cues, slower for farthest ones, and even still at the vanishing point. It can also be hypothesized that cognitive load is added by the more complex perception of 3D flows. The combination of the automatic ocular responses with the rapid postural reactions is a global strategy for balance adaptation. The study proves that 3D visual flows (because they induce measurable and specific responses) are a pertinent tool for richer immersive protocols for balance analysis and rehabilitation.

Figure 1 .

 1 Figure 1. Ocular opto-kinetics responses signed OKN : count (left -right) and (up -down). Boxes represent central quartiles (50%) for horizontal (green) and vertical (red) visual flows, for all 2D and 3D conditions.

Corresponding Author (olivier.martin@ujf-grenoble.fr)


Raphaël Groscot

Laurent D Cohen

Deformable Voxel Grids for Shape Comparisons

Keywords: Shape morphing, deformable models, generative 3D modeling

We present Deformable Voxel Grids (DVGs) for 3D shapes comparison and processing. It consists of a voxel grid which is deformed to approximate the silhouette of a shape, via energy-minimization. By interpreting the DVG as a local coordinates system, it provides a better embedding space than a regular voxel grid, since it is adapted to the geometry of the shape. It also allows to deform the shape by moving the control points of the DVG, in a similar manner to the Free Form Deformation, but with easier interpretability of the control points positions. After proposing a computation scheme of the energies compatible with meshes and pointclouds, we demonstrate the use of DVGs in a variety of applications: correspondences via cubification, style transfer, shape retrieval and PCA deformations. The first two require no learning and can be readily run on any shapes in a matter of minutes on modest hardware. As for the last two, they require to first optimize DVGs on a collection of shapes, which amounts to a pre-processing step. Then, determining PCA coordinates is straightforward and brings a few parameters to deform a shape.

INTRODUCTION

Three dimensional shapes are difficult to compare to one another, because they lack a good, canonical basis of representation. On the one hand are surfacic representations: pointclouds and meshes. Pointclouds are unordered sets, so comparing two requires a registration step which essentially determines point-to-point correspondences. This matching can operate under different assumptions: for instance, ICP [START_REF] Besl | Amethod for registration of 3-D shapes[END_REF] and variants [START_REF] Sato | 3D Face Recognition without Using the Positional Relation of Facial Elements[END_REF] for rigid affine transformations, or Earth Mover's Distance [START_REF] Fan | A point set generation network for 3D object reconstruction from a single image[END_REF] for minimal transport-cost one-to-one matching. The same holds for meshes, but the explicit connectivity also allows for spectral methods, whose local descriptors derive from eigenvalues of operators such as the Laplacian [START_REF] Ovsjanikov | Functional maps: A flexible representation of maps between shapes[END_REF][START_REF] Sun | A concise and provably informative multi-scale signature based on heat diffusion[END_REF] . On the other hand are volumetric representations: voxel grids and signed distance fields (SDF). Being scalar signals in the unit cube of ℝ ! , they indeed have a canonical embedding space. However, a big part of voxel space is non discriminative: the center (resp. the border) of the cube is mostly always occupied (resp. empty). To capture rich geometric details, they also require a sufficient grid resolution, leading to high dimensional spaces where distances are not meaningful. As for SDFs, they generally serve as a proxy to either render the shape via ray marching [START_REF] Hart | Sphere tracing: A geometric method for the antialiased ray tracing of implicit surfaces[END_REF] or generate a mesh via marching cubes [START_REF] Lorensen | Marching cubes: A high resolution 3D surface construction algorithm[END_REF] . This is why, in the context of shape editing, both these representations are mainly useful for boolean operations -intersection and union.

Instead of relying solely on their geometry, shapes can be compared using parameters which translate to meaningful properties, such as length, height, etc. In the modeling phase, this can be achieved by parametric surface or volume elements, such as splines and nurbs. But in the analysis phase, these parameters are generally not accessible. This is where shape priors come to play, either in the form of statistical distribution estimation [START_REF] Fish | Meta-representation of shape families[END_REF] , or with methods relying on deformations from a template 17 or between pairs of shapes [START_REF] Hanocka | Alignet: Partial-shape agnostic alignment via unsupervised learning[END_REF] . These are controlled by the Free Form Deformation 25 (FFD) which, although having volume-preserving properties, offers unintuitive controls. Another approach comes with neural networks, and more especially generative models such as GANs 10 and VAEs [START_REF] Kingma | Auto-Encoding Variational Bayes[END_REF] . They offer a so-called latent space which serves as a canonical, Euclidean parameter space, with a typical dimensionality lower than that of the geometric shape space, amenable to meaningful distances between points. Several works demonstrated how latent arithmetics allows for similarity clustering [START_REF] Qi | Pointnet: Deep learning on point sets for 3D classification and segmentation[END_REF][START_REF] Qi | Pointnet++: Deep hierarchical feature learning on point sets in a metric space[END_REF] , shape analogies 1 and recombinations [START_REF] Dubrovina | Composite shape modeling via latent space factorization[END_REF][START_REF] Groscot | Shape part transfer via semantic latent space factorization[END_REF] . However, they rely on heavy computations on large datasets, which not only requires powerful hardware and a long training, but also depends on the reconstruction capacity of the chosen generator architecture.

In this paper, we introduce an alternative geometric representation, which we demonstrate is adapted to shape comparisons with very simple computations: the Deformable Voxel Grid (DVG). A DVG is an energy-driven deformation of the unit cube surrounding the shape. Intuitively, if we only consider its outer surface, it consists in an elastic hull which, like a shrinking balloon, embraces the shape (see Figure 1), thus providing a low-level approximation of a given shape. It is inspired by the Topological Active Volume 2 (TAV), which is a volumetric extension of active contours [START_REF] Cohen | On active contour models and balloons[END_REF][START_REF] Kass | Snakes: Active contour mod-els[END_REF] . The unfamiliar reader can think of active contours as parametric curves which minimize a given energy, typically used for segmenting objects in images [START_REF] Hemalatha | Active Contour Based Segmentation Techniques for Medical Image Analysis[END_REF] . This energy is split into an intrinsic term -regularization -and an extrinsic term -data fidelity:

ℰ(%) = ℰ regularization (%) + ℰ data (%) (1)
This energy depends on a set of parameters % (the vertices positions for a polygonal curve), thus the minimization problem consists in finding the optimal parameters % * . In order to do so, an initial set of parameters %0 is determined manually or automatically, and they are iteratively updated via gradient descent. Intuitively, it helps to visualize this dynamics as a curve that evolves through time (each gradient descent step is a time step), hence the name active contour. For instance, if the initialization forms a closed loop around the object that needs to be segmented, the intrinsic term corresponds to a contraction force --along with regularization, and the extrinsic term to an attraction force to the contour of the object. At equilibrium, when the curve matches the contour, these two forces balance each other out. Figure 2 illustrates the evolution of an active contour. The initialization also prevents the active contour from being stuck at an undesired local minimum of the energy, by providing a close enough initial state. An active volume behaves similarly, but in three dimensions. Before drawing the analogy too far, a caveat regarding dimensions has to be noted: whereas in images (2D), an active contour is just a 1-dimensional curve, for 3D shapes, an active volume is 3-dimensional. A 3D analogy of active contours that preserves this dimensionality relationship would be an active surface. But Deformable Voxel Grids discretize the embedding space itself, by elastically deforming a regular voxel grid until its outer surface tightly embraces a given shape. The aim of this paper is not to demonstrate superior performances in a specific application, say correspondences. Rather, it is to present a unified shape representation framework, which offers natural baseline solutions to a surprising variety of problems related to deformation, among which are shape correspondences, but also retrieval of similar shapes, style transfer, and parametric editing (see Section 3). First, we present in Section 2 the DVG model, along with its estimation and post-processing.

THE DEFORMABLE VOXEL GRID MODEL

A DVG arises from the deformation of the unit cube ℝ ! which we discretize in a () + 1) × () + 1) × () + 1) grid, such that ) corresponds to the resolution, i.e. the number of subdivisions along each axis. The vertices of this grid are called control points, and their best position is determined by energy-minimization. As a matter of fact, to each state of a DVG corresponds an energy, which measures how well the DVG fits the given shape while remaining smooth. Every control point is connected to its neighbors following the 6-connectivity scheme, and every volume bounded by 8 neighbors is called a cell. Even if the faces of a cell are in general non-planar, since 4 points in 3D are not generally coplanar, they are well defined as 3D quadrilaterals. In the end, a DVG forms a hexahedral grid. Its purpose is to offer a consistent representation basis for several shapes belonging to the same class (e.g. chair or car), allowing both:

-Straightforward comparisons between shapes: the same cell (identified by its position within the grid) should correspond to the same part of a shape.

-Easy shape deformation: after attaching the shape to its optimized DVG, deforming the shape by moving the control points. Because the control points are originally close to the shape, this provides a more intuitive control of the deformation than FFD does.

Grid parameterization and energies

The parameterization of the DVG is taken from the TAV 2 . A continuous DVG is defined as V(u, v, w) = (x(u, v, w), y(u, v, w), z(u, v, w)) where 4, 5, 6 ∈ [0,1], and its corresponding energy is then:

ℰ(;) = < < < ℰ(;(4, 5, 6) . / =4 =5 =6 . / . /
where ℰ(;(4, 5, 6)) decomposes according to (1). Note that our V is discretized in a regular voxel grid, meaning that we only know the value of ;(4, 5, 6) for discrete points in [0,1] ! -corresponding to regular subdivisions of the unit cube -while the rest is interpolated using trilinear interpolation. The DVG is initialized as a regular voxel grid around the shape, and evolves through time, to find a minimal energy state. Equation ( 1) takes a generic form and must be further detailed. The energy of a given DVG state comprises three different terms with their respective relative weights:

ℰ = ℰ regularization + ℰ data = > 0 ℰ 0123456 + > 7 ℰ 708958: + > 5 ℰ 5861;35<8
The regularization energy comprises elastic and bending terms, their minimization tends to respectively shrink the grid and maintain low curvature. The data fidelity term ensures that the outer surface of the DVG is stopped by the shape, by penalizing all points of the shape that lie outside the DVG.

Elastic and bending energies. In a similar manner to active contours and topological active volumes, we penalize the squared norm of the first and second derivatives, respectively corresponding to elastic and bending energies: ) where C, A, B are coefficients which control the relative importance of each term. The elastic energy induces a contracting force, shrinking the grid inwards, while the bending energy keeps the grid as straight as possible, minimizing its curvature. To compute these first and second derivatives on the discrete parameterization, we use 3D finite differences.

Inclusion. The shape should stay inside the DVG: by design, this is the case at initialization, and this energy ensures that it remains the case during the evolution, acting as a barrier against the contraction of the DVG. Note that we only need this barrier on the surface of S. In our design and experiments, we only use sparse surface information in the form of a pointcloud uniformly sampled from a triangular mesh (with sampling weights proportional to the triangles' surface area). This allows to use the same DVG model on pointclouds and meshes alike, and simplifies the computation of this energy term. Indeed, to compute ℰ 5861;35<8 we want to determine whether each point sample is located inside V. But this on-oroff signal does not provide gradients for the gradient descent of ℰ, and we would like a stronger penalty for the farthest points. Hence a quantization scheme we devised to efficiently and differentiably estimate this inclusion for all points of S, in parallel using GPU acceleration. To test whether D ∈ ; for any D ∈ E, we resort to a family of balls {B @ (p @ , r)} @A.

B

of a given radius ), located at positions {p @ } @ , whose union provides an approximation of V, so that:

D ∈ K ⇔ ∃N, D ∈ K 5 ⇔ ∃N, |D -P 5 | = ≤ ) ⇔ =(D, {P 5 } 5 ) ≤ ) ⇔ |D -P ⋆ | ≤ )
where = is the distance between a point (D) and a set ({P 5 } 5 , 1 ≤ i ≤ l), and P ⋆ is the P 5 closest to D. A ball covering of V can easily be obtained by subdividing its cells and taking points at the centers of the newly created subcells (see Figure 3). To have a differentiable loss term, the hard inequality in ( 5) can be replaced by a soft thresholding thanks to the sigmoid

f D,F (x) = . = tanhYα(x -θ)[ + . =
, where % is the threshold and C the stiffness (the higher C, the more it behaves like a hard thresholding). It follows:

ℒ F (s ∈ V) = f G,F Yd(s, {p @ } @ )[ = f G,F (||s -p ⋆ ||) ℒ H (E ⊂ ;) = 1 `a ℒ H (D I ∈ b) I 5A. = 1 `a c J,H (||D I -P I ⋆ ||) I 5A.
This equation defines a loss corresponding to S ⊂ V, with the stiffness parameter C. This loss is used as ℰ 5861;35<8 .

Recursive subdivisions for hierarchical optimization

For a DVG of resolution ) ! cells, if r is a power of 2, say r = 2 p , we can view the grid as p successive subdivisions of a cube, corresponding to finer and finer resolution levels. This suggests a recursive optimization scheme, starting from a regular cube at resolution level 0. At level k, the position of the control points 5 I is optimized via gradient descent on energy ℰ. Then, the grid is subdivided by a factor of 2, which means that each cell is sliced into 8 smaller cells. The created vertices are located at the centers of previous faces and edges, to which a small perturbation (the residual) is added with a fading factor C I (see Figure 4a for an illustration). The recursive relationship between a resolution level 5 I and the previous one is then given by:

5 I = Sub(5 IK. ) + α I ) I (7)
where 5 I corresponds to the vertices of level k, Sub is the subdivision operator, ) I is the residual, and {α L } .MLMN the fading factors. This hierarchical optimization stabilizes the convergence to a solution close to the shape, as our experiments showed (see Figure 4b). To select precision level K for the output, one can set {α L } LMO to 1 and {α L } LPO to 0. Note that this construction, yielding a collection of v L by successive super-sampling and perturbations, is similar to a wavelet series decomposition, where each layer encodes details from increasing frequencies (in space) and decreasing amplitudes.

(

) 6
Figure 4. (Left) Each level " ( is built as the subdivision of the previous level, added to the next residual, according to Equation (7). The subdivision preserves the key points of a previous level (circled in red) and interpolates the value for the new points. The visualization is simplified by figuring color instead of position (color can be interpreted as the magnitude of a displacement). (Right) When the DVG is not optimized hierarchically (left), the edges of the original cube (thicker liners) do not align with the dominant features of the shape (both shown with same number of steps).

Registering a shape to a DVG

Once an optimal DVG V is determined for a shape S, a natural idea is to express S in coordinates (u, v, w) ∈ [0,1] ! taken from the same parameterization as ; (4, 5, 6). We call this shape registration. Given a DVG cell c and a point q inside, we want to determine its local coordinates. The trilinear interpolation f Q already used in the hierarchical subdivisions (see Section 2.2) yields a regular mapping from [0,1] ! to the cell:

∃u f, v f, w g ∈ [0,1] ! s.t. f Q (u f, v f, w g) = q
where p . , p = , … , p R are the positions of the eight vertices of c. Then, (u f, v f, w g) are the local coordinates of point q, so that one would need to invert the trilinear interpolation in order to find them. Then, an affine transformation maps the cell to its correct location within the whole DVG grid system (see Figure 5b). However, there is no analytical solution to the inversion problem, which requires numerical techniques such as Newton's method. Moreover, this inversion would be local, requiring to solve a different system for each point of the source shape, and would discard any point located outside the DVG. This is why we propose to approximate this inversion using a Thin Plate Spline 4 (TPS), which has the nice property of finding a smooth space deformation based on a set of control points.

Here, these will be the control points of the DVG, whose target positions are the equivalent points of a regular voxel grid (see Figure 5b).

APPLICATIONS AND RESULTS

Our experiments were performed on chair and car models from the ShapeNet 5 repository, with λ S = 1, λ T = 0.4, λ @ = 4, α = β = γ = 1.

(8) Figure 6. Similarity search via DVG (on 500 models). Top row is the query shape, below are the two nearest neighbors using the outer points of V as a shape descriptor.

Shape descriptor for similarity search

The positions V of a DVG encode a rough global appearance, and can serve as a shape descriptor. A nearest-neighbors search using these descriptors and a simple Euclidean distance, confirms their usefulness in querying a dataset for similar models, as depicted in Figure 6. Observe how this descriptor is blind to differences in topology, but captures the general orientation of semantical parts (back, seat, etc.).

Shape deformations: By deforming the DVG of a shape into a different configuration, one can deform the shape itself, either by using the aforementioned registration of the shape followed by a reprojection into a different grid (via trilinear interpolation), or directly via a TPS interpolator.

Style transfer: Let us consider two shapes S1 and S2, and their corresponding DVGs V1, V2. Projecting S1 into V2 performs a style transfer, in a similar fashion to AligNet 12 but without any learning -this is possible because our DVGs provide control points more adapted to the surface than AligNet's FFD grid. This use case demonstrates why we led our experiments on a chair dataset. They are strong candidates for our DVG model because:

-they generally have strong reflection symmetries; -most details that make a chair different from another one are high resolution ones: the general aspect of a chair is not very varied (depicted in the fact that the DVG elastic hulls do not widely differ one from another).

Most of the existing work in style transfer [START_REF] Lun | Elements of style: Learning perceptual shape style similarity[END_REF][START_REF] Lun | Functionality preserving shape style transfer[END_REF] applies the specific (high level) details of a source shape to a target shape, while maintaining the global proportions of the target. We take an opposite view, by applying the low level information and maintaining the high level details. Our results, presented in Figure 7, show that this effectively creates meaningful objects, in two ways: the result is easy to anticipate, and corresponds to an interpretable object. New meanings for shapes can be discovered: for instance, the conformation of a chair to a sofa creates a bench (first column), which is not present in the dataset. PCA deformations: We found that the major modes of variations for V in a dataset (the first principal components) have intuitive interpretations: for instance with chairs, the first two correspond to horizontal/vertical ratio. So, one can explore the neighborhood in PCA space of a DVG while simultaneously deforming the underlying shape. This enables an interactive shape editor where a designer can deform a shape according to intuitive parameters controlled by sliders.

Shape correspondences

Cubified shapes tend to have similar parts in similar locations, which suggests a potential for estimating shape correspondences. In order to demonstrate the versatility of our representation, we show that a naive approach already yields meaningful correspondences. In a cubified pair YS o , T q [, source and target, every point x f ∈ T q is matched to the closest Qualitative examples of such correspondences are presented in Figure 9.

CONCLUSION

By their adaptive discretization of the embedding space, Deformable Voxel Grids offer a variety of applications for 3D shapes. They allow a natural formulation of style transfer, which effectively replaces more complex approaches relying on neural networks. While most of our results involve chairs, because of their general appearance -notably, their reflection symmetries, we would like to investigate the usefulness of DVGs for other types of shapes. For instance, we expect them to display similar results on tables, and wonder about their applications on planes (a potential hurdle being the presence of wings).

For future work, we would also like to further analyze how cubification helps improve the performance of already-existing methods. For instance, our naive correspondences could be replaced by more advanced methods (e.g. functional maps [START_REF] Ovsjanikov | Functional maps: A flexible representation of maps between shapes[END_REF] ), and it would be useful to test whether the correspondences obtained on a dataset can be improved with a cubification preprocessing.

Finally, cubification can also be considered as a dataset normalization step, and one could see how a classifier/segmenter neural network could benefit from it. In fact, we think that even generative networks could use this shape representation: for instance, they could learn to output a (DVG, cubified shape) pair, which would allow to condition the generation by desired style -and not only class, as is currently the case.

Figure 1 .

 1 Figure 1. DVGs on different shape categories, for pointclouds and meshes (left: volumetric slice showing the inner cells).

Figure 2 .

 2 Figure 2. Evolution of active contour (left) versus active volume (right), depicted in 2D for clarity.

ℰ

  0123456 (;) = α(|; ; (4, 5, 6)| = + |; > (4, 5, 6)| = + |; ? (4, 5, 6)| = ) ℰ 708958: (;) = A(|; ;; (4, 5, 6)| = + |; >> (4, 5, 6)| = + |; ?? (4, 5, 6)| = ) + B(|; ;> (4, 5, 6)| = + |; >? (4, 5, 6)| = + |; ;? (4, 5, 6)| =

Figure 3 .

 3 Figure 3. During the computation of the energy ℰ !"#$%&!'" , each DVG cell is replaced by a set of regularly spaced balls of constant radius. For big enough radii, the union of the balls achieves an approximate covering of the cell.

Figure 5 .

 5 Figure 5. (Left) A natural way of setting grid coordinates on a quadrilateral is via bilinear interpolation, which maps regular subdivisons of [0,1] 2 onto the quad cell (left to right). Determining the local coordinates of a given point within the cell corresponds to inverting this interpolation (right to left). (Center) The same is done for registering a point inside a DVG, but in 3D, with the inversion of a trilinear interpolation. (Right) Examples of cubified shapes (positions in [0,1] 3 are color-coded).

Figure 7 .

 7 Figure 7. Style transfer performed via DVGs, via a TPS interpolator. All DVGs involved were automatically optimized using the same hyper-parameters. Cubification: A special case of shape deformation is cubification -the target DVG is a straight cube. For a single-class dataset, cubification provides a consistent way of representing an object from this class; examples are shown in Figure 5c. Cubification serves further purposes, such as correspondences (see Section 3.3).

Figure 8 .

 8 Figure 8. Having encoded k = 500 chairs with DVGs, a PCA on {V + } + yields principal modes of deformations, applied to deform any shape. For example in this chair dataset, they correspond to vertical and horizontal elongations (original shape on central column; + ! is the i-th principal component, the color gradient corresponds to the deviation from the shape's DVG).

  y ⋆ r ∈ S o with respect to the Euclidean distance. Hence, for the original shapes, if we denote CS (resp. CT) the cubification of S (resp. T), every x ∈ T is matched to the solution of argmin U∈W |C X (x) -C W (y)| = .

Figure 9 .

 9 Figure 9. Shape correspondence pairs (Source, Target), estimated on cubified shapes and transferred on the original models (identified by color).

ACKNOWLEDGEMENT

This work was funded in part by the French government under management of Agence Nationale de la Recherche as part of the "Investissements d'avenir" program, reference ANR-19-P3IA-0001 (PRAIRIE 3IA Institute).