@techreport{TR-IC-15-02,
   number = {IC-15-02},
   author = {Rachid Rebiha and Arnaldo V. Moura},
   title   =   {Invariants-based  Architecture  for  Semantic  Malware 
                   Resistance},
   month = {January},
   year = {2015},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 36 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       In this work we provide \emph{theoretical basis} for the design
       of  static  and  dynamic  platforms that can exhibit a suitable
       architecture  for  automatic in-depth malware analysis. We show
       how   formal  methods  involving  static  and  dynamic  program 
       analysis,   decision   procedures  and  automated  verification 
       techniques  can be used to build such architectures. We present
       automatic  formal  specification,  classification and detection
       methods  for  malware  analysis.  We provide several methods to
       generate  \emph{formal malware signatures} capable of capturing
       and  modelizing  the  core of the malicious behavior in a sound
       and   concise   way.   We  propose  to  generate  \emph{malware 
       invariants  and  abstract  models}  directly from the specified
       malware  code  in  order  to  use them as \emph{semantic aware}
       signatures.   Importantly,   these  invariants  and  abstracted 
       structures  would  remain  unchanged  in many \emph{obfuscated}
       versions  of the code. Then, we present formal model extraction
       methods in order to modelize the program being inspected. These
       computational  models  are  basically  abstract call graphs and
       pushdown  systems  annoted  with invariants at each system call
       locations.  Thus,  for  each  specification  methods and formal
       models introduced, we are able to reduce the problem of malware
       detection  to  classical  problem  very standard for the formal
       method  research  community. We also present a \emph{host-based
       intrusion  detection  systems}, where system calls are preceded
       by  the  check  of  pre-computed  invariants. We prove that any
       malware analysis or intrusion detection system will be strongly
       re-enforced  by  the  presence  of pre-computed invariants, and
       will  also  be weakened by their absence. The research security
       community  will benefit from mathematical formalisms that could
       serve as a scientific basis for their classification. The other
       main  purpose  of  this  paper  is to enlight the formal method
       research  community about writing static malware analyzer using
       several formal techniques and combined logics.
  }
}