How to Build Your Own ASP-based System?!

Answer Set Programming, or ASP for short, has become a popular and sophisticated approach to declarative problem solving. Its popularity is due to its attractive modeling-grounding-solving workflow that provides an easy approach to problem solving, even for laypersons outside computer science. However, in contrast to ASP’s ease of use, the high degree of sophistication of the underlying technology makes it even hard for ASP experts to put ideas into practice whenever this involves modifying ASP’s machinery. For addressing this issue, this tutorial aims at enabling users to build their own ASP-based systems. More precisely, we show how the ASP system clingo can be used for extending ASP and for implementing customized special-purpose systems. To this end, we propose two alternatives. We begin with a traditional AI technique and show how metaprogramming can be used for extending ASP. This is a rather light approach that relies on clingo’s reification feature to use ASP itself for expressing new functionalities. The second part of this tutorial uses traditional programming (in Python) for manipulating clingo via its application programming interface. This approach allows for changing and controlling the entire model-ground-solve workflow of ASP. Central to this is clingo’s new Application class that allows us to draw on clingo’s infrastructure by customizing processes similar to the one in clingo. For instance, we may apply manipulations to programs’ abstract syntax trees, control various forms of multi-shot solving, and set up theory propagators for foreign inferences. A cross-sectional structure, spanning meta as well as application programming, is clingo’s intermediate format, aspif, that specifies the interface among the underlying grounder and solver. We illustrate the aforementioned concepts and techniques throughout this tutorial by means of examples and several nontrivial case studies. In particular, we show how clingo can be extended by difference constraints and how guess-and-check programming can be implemented with both meta and application programming.

Verification of Program Transformations with Inductive Refinement Types

High-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking, and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing the expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference, etc.) showing that we can effectively verify stated properties.

DSM: Delayed Signature Matching in Deep Packet Inspection

Deep Packet Inspection (DPI) is widely used in network management and network security systems. The core part of existing DPI is signature matching, and many researchers focus on improving the signature-matching algorithms. In this paper, we work from a different angle: The scheduling of signature matching. We propose a Delayed Signature Matching (DSM) method, in which we do not always immediately match received packets to the signatures since there may be not enough packets received yet. Instead, we predefine some rules, and evaluate the packets against these rules first to decide when to start signature matching and which signatures to match. The predefined rules are convenient to create and maintain since they support custom expressions and statements and can be created in a text rule file. The correctness and performance of the DSM method are theoretically analyzed as well. Finally, we implement a prototype of the DSM method in the open-source DPI library nDPI, and find that it can reduce the signature-matching time about 30∼84% in different datasets, with even smaller memory consumption. Note that the abstract syntax trees (ASTs) used to implement DSM rule evaluation are usually symmetric, and the DSM method supports asymmetric (i.e., single-direction) traffic as well.

Detection of Obfuscated Javascript Code Based on Abstract Syntax Trees Coloring

The paper deals with a problem of the obfuscated JavaScript code detection and classification based on Abstract Syntax Trees (AST) coloring. Colors of the AST vertexes and edges are assigned with regard to the types of the AST vertexes specified by the program lexical and syntax structure and the programming language standard. Research involved a few stages. First of the all, a non-obfuscated JavaScript programs dataset was collected by the public repositories evaluation. Secondly, obfuscated samples were created using eight open-source obfuscators. Classifier models were built using an algorithm of gradient boosting on the decision trees (GBDT). We built two types of the classifiers. The first one is the model that classifies the program according to the type of the obfuscator used, i.e. based on what obfuscator created the sample. The second one tries to detect samples obfuscated by the obfuscator whose samples are not observed during training. The quality of the obtained models is on par with the known published results. The feature engineering method proposed in the paper does not require a preliminary analysis of the obfuscators and obfuscating transformations. In the final part of the paper we analyze a quality of models estimated, discussing the certain statistical properties of the obfuscated and non-obfuscated samples obtained and corresponding colored ASTs. Analysis of generated samples of obfuscated programs has shown that the method proposed in the paper has some limitations. In particular, it is difficult to recognize minifiers or other obfuscating programs, which change the lexical structure to a greater extent and the syntax to a lesser extent. To improve the quality of detection of this kind of obscuring transformations, one can built combined classifiers using both the method based on the AST coloring and the additional information about lexemes and punctuation, for example, entropy of identifiers and strings, proportion of characters in upper and lower case, usage frequency of certain characters etc.