# Program Behavior Analysis and Clustering using Performance Counters

Sai Praveen Kadiyala  I2R, A*STAR, Singapore<EMAIL_ADDRESS>,  Akella
Kartheek  BITS-Pilani Hyderabad, India<EMAIL_ADDRESS>and  Tram
Truong-Huu  I2R, A*STAR, Singapore<EMAIL_ADDRESS>
(2020)

###### Abstract.

Understanding the dynamic behavior of computer programs during normal working
conditions is an important task, which has multiple security benefits such as
the development of behavior-based anomaly detection, vulnerability discovery,
and patching. Existing works achieved this goal by collecting and analyzing
various data including network traffic, system calls, instruction traces, etc.
In this paper, we explore the use of a new type of data, performance counters,
to analyze the dynamic behavior of programs. Using existing primitives, we
develop a tool named perfextract to capture data from different performance
counters for a program during its startup time, thus forming multiple time
series to represent the dynamic behavior of the program. We analyze the
collected data and develop a semi-supervised clustering algorithm that allows
us to classify each program using its performance counter time series into a
specific group and to identify the intrinsic behavior of that group. We carry
out extensive experiments with $18$ real-world programs that belong to $4$
groups including web browsers, text editors, image viewers, and audio players.
The experimental results show that the examined programs can be accurately
differentiated based on their performance counter data regardless of whether
programs are run in physical or virtual environments.

Performance counters, Dynamic behavior analysis, Time series clustering

††copyright: acmcopyright††journalyear: 2020††conference: DYNAMICS 2020:
DYnamic and Novel Advances in Machine Learning and Intelligent Cyber Security
(DYNAMICS) Workshop; Dec. 07, 2020; Texas, USA††booktitle: DYNAMICS 2020:
DYnamic and Novel Advances in Machine Learning and Intelligent Cyber Security
(DYNAMICS) Workshop, Dec. 07, 2020, Texas, USA††price: 15.00††ccs: Security
and privacy Malware and its mitigation††ccs: Security and privacy
Intrusion/anomaly detection and malware mitigation

##  1\. Introduction

The latest trends in program analysis show an increase in emphasis on the
dynamic approach compared to the static approach (Or-Meir et al., 2019). In
the dynamic approach, programs are executed in a controlled environment and
their behavior is observed during the execution time. The interaction of
programs with the operating system (OS) and generated data during the
execution are collected and analyzed. High-level features such as application
programming interface (API) calls, network traffic and registry changes have
demonstrated the effectiveness (Salehi et al., 2017; Zhang et al., 2020; Das
et al., 2016; Mathew and Kumara, 2018). However, programs are increasingly
sophisticated, especially malicious programs (malware), which usually exhibit
evasive behavior when being run in a controlled execution environment. This
motivates the research community to explore the use of low-level features such
as performance counters as they are more resistant to external attacks
(Dinakarrao et al., 2019; Harris et al., 2019; Tahir et al., 2019).
Performance counters have been initially introduced for the purpose of
analyzing complex systems for debugging related issues. With the help of
available digital logic that increments the counters after the occurrence of a
specific event, these counters keep track of various micro-architectural
events, thus enabling dynamic monitoring of program behavior. We believe that
performance counter-based profilers give deeper insights into system dynamics
with lower overhead compared to their software profiler counterparts.
Nevertheless, performance counter data also has its own drawback related to
the non-determinism characteristic: several performance counters generate
different values at different execution times (Das et al., 2019). This makes
the program analysis task based on performance counters more challenging, thus
requiring a more robust approach.

Advocating the use of performance counters, we carry out in this work an
empirical study on program behavior analysis using a machine learning
technique. We propose a data collection approach that could overcome the
drawback of performance counter data discussed above. Precisely, rather than
collecting performance counters data just at only one time instant and use
this data as the sole input for analysis, we propose to collect performance
counters of a program over a long period (e.g., during startup time of the
program), thus forming a time series for each performance counter. We note
that while there exist a large number of performance counters, we focus on
per-program performance counters, which count the number of micro-
architectural events triggered by a specific program. We use a machine
learning technique to learn not only the correlation between performance
counters but also the change in the pattern of a specific performance counter
over time. This approach allows us simultaneously to represent the spatial-
temporal correlation and to identify the intrinsic dynamic behavior of each
program through its performance counter time series. While collecting
performance counter data is an easy task, labeling data to use in supervised
learning techniques is not straightforward due to the involvement of large
man-hours and the requirement of specific domain knowledge. Thus, we adopt a
clustering algorithm, which is a semi-supervised learning technique, to
classify programs based on their performance counter time series into
different groups, each having different dynamic behavior. The contribution of
our work is summarized as follows.

  * •

We develop a tool named perfextract using existing primitives
(TypePerf111TypePerf: https://ss64.com/nt/typeperf.html) to collect data from
various performance counters during a specific time window, e.g., during
startup time of programs. We note that while TypePerf has been developed to
collect data from a performance counter at a given time instant, perfextract
allows us to simultaneously collect data from various performance counters and
form time series for each counter. This allows us to capture the behavior of
each performance counter over time. We also note that there exist $28$ per-
program performance counters in Windows operating systems, we collect data
from $23$ counters since the remaining $5$ counters are not useful for our
work.

  * •

We use a semi-supervised clustering algorithm, seeded $k$-means clustering, to
classify programs, each being represented by multiple time series of
performance counters, into different groups. We also adopt seeded $k$-means
clustering to develop a new algorithm that detects whether a new program has
been installed or deviated from its “normal” behavior. We analyze the dynamic
behavior of each program group based on the changes in each performance
counter over time.

  * •

We carry out extensive experiments with $18$ real-world Windows programs
belonging to $4$ groups: web browsers, text editors, image viewers, and audio
players. We run these programs in both physical and virtual environments and
use perfextract to collect data before doing analysis.

The rest of paper is organized as follows. In Section 2, we discuss related
work on dynamic analysis of programs using both high-level and low-level
features. In Section 3, we describe our data collection framework and dynamic
behavior analysis technique. In Section 4, we present the experiments with
various scenarios and analysis of results before we conclude the paper in
Section 5.

##  2\. Related Work

Characterizing the behavior of programs based on their dynamic features is an
established methodology in the field of system security. In (Salehi et al.,
2017), Salehi et al. used API call return value recorded during the runtime of
a program as features in modeling the program behavior. In a novel fashion,
Zhaoqi et al. used API calls along with their arguments for analyzing program
behavior (Zhang et al., 2020). In (Das et al., 2016), Das et al. developed a
semantics-based online malware detection approach based on API call sequences.
In (Mathew and Kumara, 2018), an RNN-LSTM model has been developed for program
analysis. The authors used the top-ranked API call sequences based on their
Term Frequency and Inverse Document Frequency (TF-IDF).

There also exist several works that used low-level features for program
behavior analysis. In (Dinakarrao et al., 2019), Dinkarrao et al. used
performance counter data to craft adversarial attacks on malware detectors.
The authors focused on malware in Linux operating systems (OS), which has less
attraction compared to Windows OS. In (Harris et al., 2019), Harris et al.
used the performance counter data for understanding the cyclic interference
caused by cache contention, thereby detecting external attacks. In (Tahir et
al., 2019), the authors proposed to use performance counter data for profiling
of web browsers during their runtime and detecting obfuscation codes hidden in
web browsers. The authors demonstrated the effectiveness of the proposed
approach with Linux OS. In (Patel et al., 2017), Nisarg et al. used
performance counters along with machine learning models for malware detection
in Linux OS. The authors used a statistical-based methodology to select the
performance counters that are to be monitored. Similarly, in (Ozsoy et al.,
2016), Ozosoy et al. developed a malware-aware processor (MAP), which has a
dedicated component to detect malware based on performance counters. In (Tang
et al., 2014), Tang et al. used performance counter data to differentiate the
behavior of two Windows applications: Internet Explorer and Adobe Acrobat
Reader. On one hand, most of the above works (except (Tang et al., 2014))
focused on Linux OS. On the other hand, they did not consider the changes in
performance counters over time. In this work, we consider programs running in
Windows OS and develop an approach that considers the spatial-temporal
correlation of performance counter data in the form of time series. This may
overcome the effect of non-determinism of performance counter data.

##  3\. Program Behavior Analysis and Clustering Framework

In this section, we present the proposed framework for program behavior
analysis and clustering. We start with an overview description and then
describe the details of framework implementation and algorithm.

###  3.1. Framework Overview

Figure 1. Framework overview.

In Fig. 1, we depict the proposed framework, which consists of two components:
data collection and program clustering. In the data collection component, we
build up a program execution environment (e.g., a Windows virtual machine
running in Oracle VirtualBox) with the perfextract tool integrated. This
allows us to quickly refresh the environment after completing the analysis of
each program. Given a program to be analyzed, we detonate the program in the
execution environment and trigger the perfextract tool to collect performance
counter data. The output of the data collection component is a set of time
series that will be analyzed by a clustering algorithm.

We advocate for clustering algorithms to classify programs into different
groups since they do not need a labeled dataset, which could be hard to obtain
in practice. We adopt $k$-means clustering to classify each program based on
its time series of performance counters into different groups. We assume that
there would be a normal working period that all the programs exhibit their
normal behavior. The collected data during this normal working period creates
the seeding clusters (e.g., the three clusters as shown on the right side of
Fig. 1 and allows us to process new samples during the inference phase). Given
a new data sample, the clustering algorithm will identify the best cluster
that the sample belongs to. If the distance to the nearest cluster is larger
than a threshold, the sample will form a new cluster, indicating that the
program has not been recognized by the clustering algorithm. This can be due
to two reasons: either the program has been newly installed in the system and
it was run for the first time or the program has changed its behavior due to
updates or security attacks.

###  3.2. Extraction of Performance Counter Data

We now present the details of the extraction of performance counter data using
the perfextract tool. We note that the number of performance counters could
vary depending on the operating system run on the analyzing host. In Windows
OS, there is a total of $28$ per-program performance counters that can be
collected. However, during our experiments, we realized that there are $5$
counters whose values do not change over time. We decided to not collect the
data from those counters as they do not contribute to differentiating the
programs. The description of the remaining $23$ performance counters is given
in Table 1.

Table 1. Description of Per-program Performance Counters No. | Performance Counter | Description
---|---|---
1 | %Privileged Time | Percentage of elapsed time that the program spent for executing code in privileged mode
2 | Handle Count | The total number of handles currently opened
3 | IO Read Operations/sec | The rate of read operations issued by the program
4 | IO Write Operations/sec | The rate of write operations issued by the program
5 | IO Data Operations/sec | The rate of read and write IO operations
6 | IO Other Operations/sec | The rate of IO operations other than read and write operations issued by the program
7 | IO Read Bytes/sec | The byte rate of read IO operations
8 | IO Write Bytes/sec | The byte rate write IO operations
9 | IO Data Bytes/sec | The byte rate of read and write IO operations
10 | IO Other Bytes/sec | The byte rate of IO operations other than read and write issued by the program
11 | Page Faults/sec | The rate of page faults occurred during its execution
12 | Page File Bytes Peak | Maximum number of bytes used in the paging file(s)
13 | Page File Bytes | Current number of bytes used in the paging file(s)
14 | Pool Paged Bytes | Current number of bytes in the paged pool
15 | Pool Non-paged Bytes | Current number of bytes in the non-paged pool
16 | Private Bytes | Current number of bytes that are not shared with other programs
17 | Priority Base | Current base priority of the program
18 | Thread Count | Number of threads currently active in the program
19 | Virtual Bytes Peak | Maximum number of bytes of virtual address space used by the program
20 | Virtual Bytes | Current number of bytes of the virtual address space used by the program
21 | Working Set Peak | Maximum number of bytes in the set of memory pages touched by the program
22 | Working Set | Current number of bytes in the set of memory pages touched by the program
23 | Working Set - Private | Current number of bytes in the set of memory pages exclusively touched by the programs

For each performance counter, perfextract periodically collects its value
using a primitive available for Windows OS, i.e., TypePerf. The time interval
between collection instants is predefined (e.g., every $1$ second) so as to
not cause significant overhead (i.e., query the values too frequently) or miss
the behavior changes of the counter (i.e., the interval is too long). We also
define a time window for the collection duration so that the performance
counters of each program will be collected in a specific duration, e.g., $30$
seconds. It is worth mentioning that it may be useful to collect the data for
the entire execution duration of the program as the more data collected, the
better the representation of program behavior. However, the execution duration
of each program depends on the nature of its application and usage behavior of
users, leading to heterogeneous execution duration of programs. For instance,
a user may use a web browser for a few minutes for entertainment but he may
use a text editor for hours to work. Nevertheless, if the time window is too
short we may not have sufficient data for analyzing program behavior.
Furthermore, to avoid the bias from the usage behavior of users, we collect
the performance counter data during the start time of programs, e.g., during
the first $30$ seconds when programs are launched. In actual implementation,
we can use a program monitor to trigger perfextract when a program is started.
Collection of performance counter data at the start time of programs may work
well with benign programs that do not exhibit evasive behavior. Thus, there is
a need for a more advanced approach (e.g., using a random collection) to avoid
such an evasive behavior. We keep this task for future work when we work with
malware samples.

Consequently, we obtain $23$ time series, each having multiple values (e.g.,
$30$ values collected over $30$ seconds) representing the temporal evolution
of a performance counter. By analyzing the time series, we analyze the
temporal behavior of performance counters rather than comparing a particular
value of performance counter among programs. While two programs may have the
same temporal behavior of certain performance counters, they may differ from
each other by the time series from the other performance counters. With the
support of machine learning that could learn the correlation from multi-
dimensional data with both temporal and spatial correlation, we use
performance counter time series to cluster programs into different groups,
each having similar behavior. As discussed in the introduction, this could
help one to identify unauthorized programs installed in the systems or detect
abnormal behavior of a particular program, which has been previously installed
and run in the system.

###  3.3. Program Clustering and Fingerprinting

In this section, we present an algorithm that analyzes the data collected from
performance counters as presented in the previous section to perform program
clustering and fingerprinting. By clustering, we mean that computer programs
are classified into different groups based on their functionalities tied to
the performance counter values, e.g., text editors, web browsers, audio
players, and image viewers. We refer to this clustering approach as coarse-
grained clustering. By fingerprinting, we perform fine-grained clustering of
data samples (i.e., each data sample is a set of time series) collected at
different time instants of a particular program so as to identify the program
by its performance counter data. Obviously, the number of groups (clusters) in
the fine-grained clustering approach is much larger compared to that of the
coarse-grained approach. Given the number of program groups and the total
number of programs installed in the system, we use a conventional clustering
algorithm such as $k$-means clustering to process the data. We note that
$k$-means clustering algorithm aims at minimizing the total distance of every
data sample to its cluster centroid. Given a dataset to be classified into $k$
groups where $k$ is provided as an input, the partition of the samples in the
dataset is achieved by minimizing the following objective function:

(1) $\displaystyle\sum_{i=1}^{k}\sum_{x\in\mathcal{G}_{i}}||x-\mu_{i}||^{2}$

where $\mu_{i}$ is the centroid of cluster $\mathcal{G}_{i}$. Seeded $k$-means
(Basu et al., 2002) is a semi-supervised clustering algorithm based on
$k$-means. It used a small set of labeled data to initialize $k$-means in
computing the centroids rather than choosing a random number of clusters.

Algorithm 1 clusterProgram($\mathcal{X}$)

1:$\mathcal{X}$ $\triangleright$ time series of performance counter data

2:$\mathcal{D}$ $\triangleright$ existing labeled data samples

3:$\mathcal{C}$ $\triangleright$ Cluster of the input sample

4:$\\{\mathcal{G},d\\}\leftarrow\texttt{getNearestCluster}(\mathcal{X},\mathcal{D})$

5:if $d<\beta$ then $\triangleright$ $\beta$ is a predefined threshold

6: Add sample $\mathcal{X}$ to cluster $\mathcal{G}$

7:else

8: Create a new cluster

9:end if

In Algorithm 1, we present the adopted clustering algorithm for program
clustering. Given a data sample that includes $23$ time series of $23$
respective performance counters, the algorithm starts by identifying the
nearest cluster for the sample based on the distance from the sample to the
centroid of the cluster. This step is performed by line 4 in Algorithm 1. The
output of the function getNearestCluster($\mathcal{X},\mathcal{D}$) is the
index of the nearest cluster ($\mathcal{G}$), and the distance between the
sample and the centroid of the cluster ($d$), normalized based on the samples
in the nearest cluster. If the distance is smaller than a predefined threshold
($\beta$), the sample is considered part of the cluster. Otherwise, it will
form a new cluster, which indicates that a new program has been executed or a
previously-seen program has deviated from its normal behavior. It is to be
noted that the function getNearestCluster($\mathcal{X},\mathcal{D}$) will
compute the distance from sample $\mathcal{X}$ to all the seeding clusters.
There may exist multiple seeding clusters that are close to sample
$\mathcal{X}$ with a distance smaller than $\beta$. The function will return
the closest cluster to the sample. The challenging issue is how to determine
the threshold to decide whether a program is newly-installed in the system or
it deviates from its previous behavior. A naive approach is to set $\beta=1$,
corresponding to the distance from the centroid to the farthest data sample of
the nearest cluster. However, this approach may not work well in practice due
to the non-linear characteristic of the multi-modal data and the clusters are
not in a spherical shape. There exist in the literature other approaches that
can be used to compute the distance from a samples to a cluster centroid such
as Euclidean distance or $z$-score (Thangavelu et al., 2019). We note that
Algorithm 1 can be used for both cases: coarse-grained clustering and fine-
grained clustering with a minor change in the parameter $k$ of the seeded
$k$-means clustering algorithm.

##  4\. Experimental Results

In this section, we present various experiments carried out to demonstrate the
effectiveness of the proposed approach. We first present the experimental
setup and the programs used in our experiments before we present the analysis
of results.

###  4.1. Experimental Setup and Programs

Table 2. Programs Used in Experiments No. | Domain | Programs | #Samples
---|---|---|---
1 | Text editor | Atom, gVim, Notepad, | 20 each
Notepad++, Sublime Text
2 | Web browser | Brave, Google Chrome, | 20 each
Internet Explorer, Vivaldi,
Firefox
3 | Image viewer | WildBit, ImageGlass, | 20 each
FastStone, MS Paint,
XnView
4 | Audio player | Clementine, | 20 each
foobar2000, VLC

(a) Time series of Handle Counts (b) Time series of page file bytes

Figure 2. Time series of performance counter data of various programs.

We carried out all the experiments in a virtual machine with 16GB RAM and
Windows 10 Operating System using Oracle VirtualBox. We implemented
perfextract in Python, which also provides various libraries for data
processing and analysis. We used $18$ popular programs belonging to $4$
application domains including text editors, web browsers, image viewers, and
audio players. The selected programs are presented in Table 2. For each of the
programs, we collected $20$ data samples by launching the program with $20$
different input arguments, e.g., opening a web browser with $20$ randomly-
chosen websites or launching a text editor with $20$ different text files. It
is worth mentioning again that each data sample includes $23$ time series of
performance counters presented in Table 1, each having $30$ values for a
duration of $30$ seconds. Furthermore, to reduce the bias of the data to any
particular run, for each input argument, we executed the monitored program
(e.g., text editor, web browser) ten times, each commencing at a random
instance in time. This increases the randomness of data so that the machine
learning algorithms will learn the data pattern (i.e., the temporal behavior
of programs) rather than a particular value. Consequently, we have collected
$3600$ ($18\times 20\times 10$) data samples for $18$ programs, which will be
used for the experiments. In Fig. 2, we plot the time series of two
performance counters (i.e., Handle Counts and Page File Bytes) of various
programs. We see that there is a significant separation in the behavior of the
performance counter data among programs. This allows machine learning
algorithms to learn program behavior and differentiate them efficiently.

###  4.2. Analysis of Results

####  4.2.1. Coarse-grained and Fine-grained Clustering.

(a) Coarse-grained intra-cluster distance. (b) Coarse-grained inter-cluster
distance.

Figure 3. Box plot representation for intra-cluster and inter-cluster
distances with coarse-grained approach.

In this experiment, we fed all $3600$ data samples to the clustering algorithm
($k$-mean clustering), given the number of clusters (i.e., $4$ clusters in
case of coarse-grained clustering and $18$ clusters in case of fine-grained
clustering). In Fig. 3 and Fig. 4, we present the box plot representation of
intra-cluster and inter-cluster distances for the clusters resulted from the
clustering algorithm. The intra-cluster distance of a cluster is computed as
the mean of the distance from all the samples belonging to the cluster to its
centroid. The inter-cluster distance of a cluster is computed as the mean of
the distance from its centroid to the centroid of the remaining clusters. As
expected, the intra-cluster distance of most of the clusters is smaller than
the inter-cluster distance. We also obtained a very small standard deviation
of the distances with the fine-grained clustering scenario. This demonstrates
that data samples belonging to the same cluster have similar behavior that
allows the clustering algorithm to learn their similarity and pattern.

(a) Fine-grained intra-cluster distance. (b) Fine-grained inter-cluster
distance.

Figure 4. Box plot representation for intra-cluster and inter-cluster
distances with fine-grained approach.

To further demonstrate the effectiveness of our clustering approach, we use
t-SNE (van der Maaten and Hinton, 2008) to produce the two-dimensional scatter
plots of the clustering results using coarse-grained and fine-grained
approaches. We note that t-SNE is a technique for visualization of high-
dimensional data by applying dimensionality reduction to the data before
plotting to a two or three-dimensional plot. In Fig. 5, the results show that
even though each group of programs is distributed at different locations,
there is a clear separation among clusters of programs and application types.
This insight provides us the motivation to develop the algorithm to detect new
programs installed in the system or behavior deviation of existing programs.

(a) Coarse-grained clustering (b) Fine-grained clustering

Figure 5. t-SNE two-dimensional plots for results obtained by clustering.

####  4.2.2. Identification of Unknown Programs

In this experiment, we evaluate the capability of the proposed approach to
detect unknown programs. Given the $18$ programs used for our experiments, we
randomly selected $4$ programs, among them $3$ programs are considered as
seeding clusters and the remaining program is considered as an unknown
program. With seeding clusters, we mean that all the data samples of the $3$
programs are analyzed by the clustering algorithm forming $3$ different
clusters whose labels are known a priori. Given a data sample of the unknown
program, we used Algorithm 1 to compute the distance between the data sample
and the centroids of the $3$ seeding clusters and determine whether a new
cluster is formed or not. If a new cluster is formed, it indicates that the
proposed approach is able to detect the unknown program executed in the
system. Otherwise, it fails to do so.

With $18$ programs, there are $12240={18\choose 3}\times 15$ experimental
instances that could be examined. We carried out the experiments with $5000$
random instances, resulting in a detection ratio of $98.7\%$. In Table 3, we
present $15$ such experimental instances, among which the proposed approach
fails to detect the unknown program in two instances. Analyzing the data of
these two instances, we observed that performance counter data of Vivaldi and
Brave (i.e., the instance in row $6$) are very close. Similar trends were also
observed in the case of row $9$ between Firefox and Internet Explorer. In
reason of this behavior could be the fact that all the web browsers use the
same rendering engine. In Fig. 6, we present several two-dimensional scatter
plots of data points randomly selected from $4$ programs using t-SNE. We
observe that there is a clear separation among clusters. We verified the
cluster index obtained by the clustering algorithm against ground truth data.
To determine the value of parameter $\beta$ (i.e., the distance threshold of
deviation), we performed a grid search in the range $[0,1]$ and selected the
value that yields the best performance.

Table 3. Selected Instances for Testing of Clustering Model No. | Experimental Instances | Result
---|---|---
Seeding Clusters | Test
1 | gVim, Notepad, Notepad++ | Atom | Detected
2 | Atom, Brave, Google Chrome | gVim | Detected
3 | Sublime Text, Google Chrome, | Notepad | Detected
Vivaldi
4 | Atom, Firefox, Vivaldi | Notepad++ | Detected
5 | Brave, Google Chrome, | Sublime | Detected
Vivaldi | Text
6 | gVim, Vivaldi, Clementine | Brave | Not
Detected
7 | Notepad, Internet Explorer, | Google | Detected
WildBit | Chrome
8 | Atom, Vivaldi, Clementine | Firefox | Detected
9 | gVim, Firefox, VLC | Internet | Not
Explorer | Detected
10 | Notepad++, FastStone, | Vivaldi | Detected
foobar2000
11 | Atom, Brave, Clementine | WildBit | Detected
12 | Sublime Text, Brave, | FastStone | Detected
Google Chrome
13 | Atom, Notepad, Vivaldi | ImageGlass | Detected
14 | Clementine, Google Chrome, | MS Paint | Detected
Internet Explorer
15 | Atom, Brave, Vivaldi | XnView | Detected

We also performed experiments of the detection of unknown programs at the
coarse-grained and fine-grained levels. At the coarse-grained level, we
considered all the seeding programs are clustered into $3$ clusters while the
unknown program should form the fourth cluster. At the fine-grained level,
there will be $17$ seeding clusters and the unknown program should form the
$18^{\text{th}}$ cluster. In Fig. 7, we present the t-SNE plots for these two
experiments with labels obtained from our clustering algorithm. The results
show that in both cases, the unknown program forms a new cluster that is well
separated from the seeding clusters.

(a) Separation among Atom, Brave, WildBit and Clementine (b) Separation among
Vivaldi, Clementine, foobar2000 and VLC

Figure 6. Two-dimensional scatter plots of various clusters using t-SNE.

####  4.2.3. Detection of Behavior Deviation

(a) Web browser samples at the coarse-grained level. (b) Firefox samples at
the fine-grained level.

Figure 7. t-SNE visualization.

(a) Page File Bytes (b) I/O Data Operations (c) Handle Counts (d) Pool Paged
Bytes

Figure 8. Various performance counter time series for normal and deviated
versions of Google Chrome.

As we discussed earlier, existing programs (that have been installed in the
systems) could change their normal behavior due to various reasons such as
updates or being tampered by viruses or attackers. While program updates may
not cause any harmful consequences, programs tampered by viruses or attackers
may lead to data loss. Thus, it is beneficial to detect such deviation as
earlier as possible. In this experiment, we demonstrate that the proposed
approach could detect such a behavior deviation. We introduced a deviation in
Google Chrome with a custom extension, which consecutively opens many photos
on the Amazon website. In Fig. 8, we present the deviation of performance
counter data (i.e., Page File Bytes, I/O Data Operations, Handle Counts and
Pool Paged Bytes) in comparison with one of the data samples collected during
its normal working conditions, i.e., the data samples collected with Google
Chrome when opening the Amazon website without the customized extension. We
used Algorithm 1 to determine whether a data sample of a program has
“significantly” deviated from its normal behavior. We have also run the
original $k$-means clustering algorithm on the dataset of Google Chrome that
included the data samples collected during normal working conditions and the
samples that are collected with the custom extension. The clustering results
show that the data samples are separately clustered into two groups. As the
label of the samples collected during normal conditions is known, the
remaining cluster includes all the data samples collected with custom
extension, representing the behavior deviation of Google Chrome.

####  4.2.4. Bare-metal vs Virtual Environment

(a) Handle Counts Time Series. (b) Page File Bytes.

Figure 9. Difference in performance counter values in virtual and physical
environment for two separate runs.

While we have done all the experiments in a virtual environment (i.e.,
executing the programs in a virtual machine and collect performance counter
time series for analysis), the proposed approach can also be applied to a
bare-metal environment. To demonstrate this, we have run the perfextract tool
in a physical host and collected the performance counter time series of the
programs. In Fig. 9, we plot the time series of two performance counters
(Handle Counts and Page File Bytes) of Google Chrome when running in a virtual
machine and in a bare-metal environment. We can observe that there is a change
in the values of the performance counters (i.e., the number of events of
Handle Counts and Page File Bytes in the virtual machine is fewer than that in
a bare-metal environment). However, evolution trends remain the same for both
environments. As we discussed earlier, the proposed approach learns not only
the dynamic behavior of a program from the values of performance counters but
also the correlation among the values through its changing trends (i.e.,
evolution trends) over time. Thus, the clustering model when deployed to the
bare metal environment may need to be retrained on the data collected in this
environment so as to adapt to the new data distribution and achieve the
desired performance.

##  5\. Conclusions

In this paper, we presented a clustering-based approach to analyze program
behavior in a given environment using performance counters. We collected the
data from various performance counters as time series and analyzed program
behavior based on temporal and spatial correlations represented by the time
series. We developed a tool to ease the collection of data using existing
primitives provided by the operation systems (e.g., Windows OS provides
TypePerf to collect the current value of a performance counter). We adopted a
conventional clustering algorithm, $k$-means clustering, to cluster programs
at both coarse-grained level (i.e., based on type of programs) and fine-
grained level (i.e., differentiating among programs). We also adopted the
algorithm to detect new/unknown programs installed in the system, as well as
behavior deviation of existing programs due to software updates or tampering
activities. We carried out experiments with $18$ programs that belong to $4$
different groups (web browsers, text editors, image viewers and audio
players). The experimental results show that the proposed approach manages to
accurately cluster programs into their respective groups. The results also
demonstrate that the proposed approach can be used to detect whether a new
program emerges (i.e., it is a newly-installed program) or an existing program
has deviated from its normal behavior. For future work, we aim at further
developing the proposed approach to perform malware detection using
performance counter time series.

###### Acknowledgements.

This research is supported by the Agency for Science, Technology and Research
(A*STAR) under its RIE2020 AME Core Funds (SERC Grant No. A1916g2047). We
would like to thank Partha Pratim Kundu, Sin G. Teo and Vasudha Ramnath for
their valuable feedback and fruitful discussion during the implementation of
this work.

## References

  * (1)
  * Basu et al. (2002) S. Basu, A. Banerjee, and R. J. Mooney. 2002.  Semi-supervised Clustering by Seeding. In _Proc. ICML 2002_. PRML, Sydney, Australia, 27–34.
  * Das et al. (2016) Sanjeev Das, Yang Liu, Wei Zhang, and Mahintham Chandramohan. 2016\.  Semantics-based online malware detection: Towards efficient real-time protection against malware.  _IEEE Trans. Inf. Forensics Secur._ 11, 2 (Feb. 2016), 289–302.
  * Das et al. (2019) Sanjeev Das, Jan Werner, Manos Antonakakis, Michalis Polychronakis, and Fabian Monrose. 2019\.  SoK: The challenges, pitfalls, and perils of using hardware performance counters for security. In _Proc. 2019 IEEE Symposium on Security and Privacy (S &P)_. IEEE, San Francisco, USA, 20–38.
  * Dinakarrao et al. (2019) Sai Manoj Pudukotai Dinakarrao, Sairaj Amberkar, Sahil Bhat, Abhijitt Dhavlle, Hossein Sayadi, Avesta Sasan, Houman Homayoun, and Setareh Rafatirad. 2019.  Adversarial attack on microarchitectural events based malware detectors. In _Proc. 2009 56th Annual Design Automation Conference_. IEEE, San Franscisco, USA, 1–6.
  * Harris et al. (2019) Austin Harris, Shijia Wei, Prateek Sahu, Pranav Kumar, Todd Austin, and Mohit Tiwari. 2019\.  Cyclone: detecting contention-based cache information leaks through cyclic interference. In _Proc. 52nd Annual IEEE/ACM International Symposium on Microarchitecture_. IEEE, Columbus, OH, USA, 57–72.
  * Mathew and Kumara (2018) J Mathew and MA Ajay Kumara. 2018.  API Call Based Malware Detection Approach Using Recurrent Neural Network—LSTM. In _Proc. International Conference on Intelligent Systems Design and Applications_. Springer, Vellore, India, 87–99.
  * Or-Meir et al. (2019) Ori Or-Meir, Nir Nissim, Yuval Elovici, and Lior Rokach. 2019\.  Dynamic malware analysis in the modern era—A state of the art survey.  _ACM Computing Surveys (CSUR)_ 52, 5 (2019), 1–48.
  * Ozsoy et al. (2016) Meltem Ozsoy, Khaled N Khasawneh, Caleb Donovick, Iakov Gorelik, Nael Abu-Ghazaleh, and Dmitry Ponomarev. 2016.  Hardware-based malware detection using low-level architectural features.  _IEEE Trans. Comput._ 65, 11 (Mar. 2016), 3332–3344.
  * Patel et al. (2017) Nisarg Patel, Avesta Sasan, and Houman Homayoun. 2017\.  Analyzing hardware based malware detectors. In _Proc. 54th ACM/EDAC/IEEE Design Automation Conference (DAC)_. IEEE, Austin, TX, USA, 1–6.
  * Salehi et al. (2017) Zahra Salehi, Ashkan Sami, and Mahboobe Ghiasi. 2017\.  MAAR: Robust features to detect malicious activity based on API calls, their arguments and return values.  _Engineering Applications of Artificial Intelligence_ 59 (2017), 93–102.
  * Tahir et al. (2019) Rashid Tahir, Sultan Durrani, Faizan Ahmed, Hammas Saeed, Fareed Zaffar, and Saqib Ilyas. 2019\.  The browsers strike back: Countering cryptojacking and parasitic miners on the web. In _Proc. IEEE Conference on Computer Communications (INFOCOM 2019)_. IEEE, Paris, France, 703–711.
  * Tang et al. (2014) Adrian Tang, Simha Sethumadhavan, and Salvatore J Stolfo. 2014\.  Unsupervised anomaly-based malware detection using hardware features. In _Proc. International Workshop on Recent Advances in Intrusion Detection_. Springer, Gothenburg, Sweden, 109–129.
  * Thangavelu et al. (2019) Vijayanand Thangavelu, Dinil Mon Divakaran, Rishi Sairam, Suman Sankar Bhunia, and Mohan Gurusamy. 2019.  DEFT: A Distributed IoT Fingerprinting Technique.  _IEEE Internet of Things Journal_ 6, 1 (Feb. 2019), 940–952.
  * van der Maaten and Hinton (2008) L.J.P. van der Maaten and G.E. Hinton. 2008.  Visualizing High-Dimensional Data Using t-SNE.  _Journal of Machine Learning Research_ 9 (Nov. 2008), 2579–2605.
  * Zhang et al. (2020) Zhaoqi Zhang, Panpan Qi, and Wei Wang. 2020.  Dynamic Malware Analysis with Feature Engineering and Feature Learning. In _Proc. 34th AAAI Conference on Artificial Intelligence_. AAAI Press, Palo Alto, California, USA, 1210–1217.


1

# Electronic Appendix to “Input Invariants”

Dominic Steinhöfel  0000-0003-4439-7129 CISPA Helmholtz Center for Information
SecurityStuhlsatzenhaus 5Saarbrücken66123Germany<EMAIL_ADDRESS>and  Andreas Zeller  0000-0003-4719-8803 CISPA Helmholtz Center for
Information SecurityStuhlsatzenhaus 5Saarbrücken66123Germany<EMAIL_ADDRESS>
In this electronic appendix to our paper “Input Invariants” (Dominic
Steinhöfel and Zeller, 2022), we provide additional examples, formal
definitions, theorems, and proof sketches. Furthermore, we show the invariants
that ISLearn mined in our evaluation (RQ3). For more information on the ISLa
language, we also refer to the ISLa language specification (Steinhöfel, 2022).

##  0\. LABEL:main-sec:isla_by_example

In LABEL:main-sec:isla_by_example, we discussed the semantic properties _def-
use_ and _redefinition_ along the XML language. Apart from those, there are
two other re-occurring _generic_ constraints we would like to discuss:
_Length_ properties and complex conditions for which we need dedicated
_semantic predicates_.

One of the target languages in our evaluation (LABEL:main-sec:evaluation) is
reStructuredText (reST)reStructuredText (reST), a plaintext markup language
used, e.g., by Python’s docutils. In reST, document (sub)titles are underlined
with “=” or “-” symbols. However, titles are only valid if the length of the
underline is not smaller than the length of the title text. This property
cannot be expressed in a Context-Free Grammar (CFG); however, we can easily
capture it in an ISLa constraint:

⬇

str.len(
.<underline>) >=

str.len(
.<title-text>)

The corresponding Core-ISLa constraint is

⬇

forall
 title=

"{<title-txt> titletxt}\n{<underline> underline}" in start:

(>= (str.len underline) (str.len titletxt))

There are properties which cannot be expressed using structural predicates and
SMT-LIB formulas alone. A stereotypical case are checksums occurring in many
binary formats, such as in the TAR archive file format from our benchmark set.
To account for such situations, we can extend the ISLa language with
additional atomic assertions, so-called _semantic predicates_. In contrast to
structural predicates such as inside or same_position, which we have seen
before, semantic predicates do not always evaluate to false for invalid
arguments. Instead, they can suggest a _satisfying solution_. The solver logic
for individual semantic predicates is implemented in Python code in our
prototype. Once this logic has been implemented, we can pass such predicates
as additional signature elements to both the ISLa evaluator or solver and use
them in constraints. The following constraint, which is part of our constraint
set for TAR files, uses a semantic predicate tar_checksum computing a correct
checksum value for the header of a TAR file.

⬇

tar_checksum(, <header..<checksum>)

This corresponds to the Core-ISLa constraint

⬇

forall  header in start:

forall <checksum> checksum in header:

tar_checksum(header, checksum)

Another use case for semantic predicates is when the SMT solver frequently
times out when looking for satisfying assignments. This happens in particular
for constraints involving a complex combination of arithmetic and string
(e.g., regular expression) constraints. For example, valid CSV files have the
property that all rows have the same numbers of columns. Assuming that we know
the number of columns in the file header, we could create a regular expression
matching all CSV lines with the same number of columns. However, if we admit
quoted expressions and a wide character range for contained text, these
regular expressions get quite complex, and the problem exceeds the
capabilities of current SMT solvers in our experience. Thus, we implemented a
new semantic predicate count which counts the number of occurrences of some
nonterminal in an input tree, and fixes trees with an insufficient number of
occurrences if possible. The following ISLa constraint for the CSV property
uses an additional language feature: It introduces a _numeric constant_ colno
using the num directive, which works similarly to let expressions in
functional programming languages. It is primarily—and also in this
example—used to enable information exchange between semantic predicate
formulas.

⬇

forall <csv-header> hline:

exists int colno: (

str.to_int(colno) >= 3 and

str.to_int(colno) <= 5 and

count(hline, "<raw-field>", colno) and

forall <csv-record> line in start:

count(line, "<raw-field>", colno))

One has to be aware that the _order_ of semantic predicates in a constraint
matters. This is in contrast to all other language atoms: SMT formulas, in
particular, are fed to an SMT solver only after all universal quantifiers have
been eliminated resp. matched, and evaluated _en bloc_. Semantic predicates,
on the other hand, are generally not compositional. When computing the
checksum for a TAR file, for instance, it is important that all elements of
the file header are already fixed at that point, i.e, all semantic predicates
on header elements have to be evaluated before. Consequently, they have to
occur before the checksum predicate in the overall constraint. Despite this
particularity, semantic predicates are an easy way to increase both the
expressiveness and solving performance of ISLa constraints, and to overcome
the limits of SMT-LIB and off-the-shelf solvers.

##  0\. LABEL:main-sec:syntax_and_semantics

We provide a more formal definition of derivation trees. We use the symbols
$<$ and $\leq$ to denote the strict and non-strict versions of the same
partial order relation, respectively; for the corresponding covering relation
which only holds between parents and their _immediate_ children, we write
$\prec$.

###### Definition 0.1 (Derivation Tree).

A _derivation tree_ for a CFG $G=(N,T,P,S)$ is a _rooted ordered tree_
$t=(X,\leq_{V},\leq_{S})$ such that  (1) the vertices $v\in{{X}}$ are
_labeled_ with symbols $\mathit{label}(v)\in{}N\cup{}T$,  (2) the _vertical_
order $\leq_{V}\,\subseteq{}X\times{}X$ indicates the parent-child relation
such that the partial order $(X,\leq_{V})$ forms an unordered tree,  (3) the
_sibling_ order $\leq_{S}\,\subseteq{}X\times{}X$ yields a partial order
$(X,\leq_{S})$ such that two distinct nodes $v_{1}$, $v_{2}$ are comparable by
relation $\prec_{S}$ if, and only if, they are siblings,  (4) the root of $t$
is labeled with $S$, and  (5) each inner node $v$ is labeled by a symbol in
$n\in{}N$ and, if $v_{1},\dots,v_{k}$ is the ordered list of all immediate
children of $v$, i.e., all distinct nodes such that $v\prec_{V}{}v_{i}$ and
$v_{i}<_{S}{}v_{l}$ for $1\leq{}i<l\leq{}k$, there is a production
$(n,s_{1},\dots,s_{k})\in{}P$ such that $\mathit{label}(v)=n$ and, for all
$v_{i}$, $\mathit{label}(v_{i})=s_{i}$.  We write $\mathit{leaves}(t)$ for the
set of leaves of $t$, and $\mathit{label}(t)$ for the label of its root. A
derivation tree is _closed_ if $l\in{}T$ for all $l\in\mathit{leaves}(t)$, and
_open_ otherwise. We define
$\mathit{closed}(t)\coloneqq\forall{}l\in\mathit{leaves}(t):l\in{}T$, and
$\mathit{open}(t)\coloneqq\neg\mathit{closed}(t)$. $\mathcal{T}(G)$ is the set
of all (closed and open) derivation trees for $G$.

###### Example 0.2.

We explain the formal definition of derivation trees (Definition 0.1) along
the XML document x. visualized in Figure LABEL:main-
fig:example_xml_derivation_tree in our paper (Dominic Steinhöfel and Zeller,
2022). Formally, this tree is represented as a triple
$t=(X,\leq_{V},\leq_{S})$, where $X=\\{v_{1},\dots,v_{14}\\}$, with
$\mathit{label}(v_{1})=\langle\mathit{xml\text{-}tree}\rangle{}$,
$\mathit{label}(v_{2})=\langle\mathit{xml\text{-}open\text{-}tag}\rangle{}$,
etc. The _vertical order_ $\leq_{V}$ contains the edges in the figure: For
example, $v_{1}\leq_{V}{}v_{2}$ and $v_{2}\leq_{V}{}v_{13}$. This relation
alone only gives us an unordered tree: When “unparsing” the tree, we could
thus obtain the undesired result xa><>. Thus, we define a _sibling order_
$\leq_{S}$ to order the immediate children of the same node. For instance, we
have $v_{6}\leq_{S}{}v_{8}$ (and $v_{6}\leq_{S}{}v_{6}$, $v_{6}<_{S}{}v_{8}$,
and $v_{6}\prec_{S}{}v_{7}$), but not $v_{6}\leq_{S}{}v_{9}$ (since they have
different parents) and $v_{6}\prec_{S}{}v_{8}$ (since they are not _immediate_
siblings). The tree is not only any ordered tree, but a _derivation tree_ for
the XML grammar in Figure LABEL:main-fig:xml-bnf in (Dominic Steinhöfel and
Zeller, 2022), since it satisfies 4 and 5 of Definition 3.4 in (Dominic
Steinhöfel and Zeller, 2022). The root of the tree, $v_{1}$, is labeled with
the grammar’s start symbol $\langle\mathit{xml\text{-}tree}\rangle{}$ (Item
(4)). The tree relations conform to the possible grammar derivations:
Consider, e.g., node $v_{2}$ and its immediate children $v_{6}$, $v_{7}$, and
$v_{8}$. According to Item (5), there has to be a production
$(\langle\mathit{xml\text{-}open\text{-}tag}\rangle{},\text{`}\texttt{<}\text{'},\langle\mathit{id}\rangle{},\text{`}\texttt{>}\text{'})$
in the grammar, which is indeed the case, since
$\text{`}\texttt{<}\text{'}\,\langle\mathit{id}\rangle{}\,\text{`}\texttt{>}\text{'}$
is an expansion alternative (the first one) for the nonterminal
$\langle\mathit{xml\text{-}open\text{-}tag}\rangle{}$. The leaf set
$\mathit{leaves}(t)$ is $\\{v_{6},v_{13},v_{8},v_{9},v_{10},v_{14},v_{12}\\}$.
The tree $t$ is _closed_ , since all leaves are labeled with _terminal_
symbols. It would be _open_ if we removed the subtree rooted in any tree node
(but the root).

#### Standard ISLa Predicates

ISLa offers a catalog of default supported predicates. Table 1 provides an
overview of those. Structural predicates can be re-used for many different
languages, while semantic predicates are mostly application-specific. For this
reason, there is only one semantic predicate included in ISLa per default,
which is the count predicate used in the formalization of CSV.

Table 1. Standard ISLa predicates. The predicate count is a semantic predicate; all other predicates are structural predicates. Predicate |  Explanation
---|---
after($\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ occurs after $\mathit{node}_{2}$ (not below) in the parse tree.
before($\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ occurs before $\mathit{node}_{2}$ (not below) in the parse tree.
consecutive($\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ and $\mathit{node}_{2}$ are consecutive leaves in the parse tree.
different_position($\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ and $\mathit{node}_{2}$ occur at different positions (cannot be the same node).
direct_child($\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ is a direct child of $\mathit{node}_{2}$ in the derivation tree.
inside($\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ is a subtree of $\mathit{node}_{2}$.
level(PRED, NONTERMINAL, $\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ and $\mathit{node}_{2}$ are related relatively to each other as specified by PRED and NONTERMINAL (see below). PRED and NONTERMINAL are strings.
nth(N, $\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ is the N-th occurrence of a node with its nonterminal symbol within $\mathit{node}_{2}$. N is a numeric String.
same_position($\mathit{node}_{1}$, $\mathit{node}_{2}$) |  $\mathit{node}_{1}$ and $\mathit{node}_{2}$ occur at the same position (have to be the same node).
count(in_tree, NEEDLE, NUM) |  There are NUM occurrences of the NEEDLE nonterminal in in_tree. NEEDLE is a string, NUM a numeric string or int variable.

#### Matching Match Expressions

Match expressions are matched against derivation trees by first parsing them
into _abstract_ parse trees (with open leaves), and then matching these parse
trees against the derivation tree in question. This process is also described
in detail in the ISLa language specification (Steinhöfel, 2022).

We use a function $\mathit{mexprTrees}(T,\mathit{mexpr})$ that takes a
nonterminal $T$ and a match expression $\mathit{mexpr}$ and returns a set of
derivation trees. If the match expression contains _optional_ elements, it is
“flattened” first. That is, we compute all combinations of activated and non-
activated optional expressions. If there are $n$ optionals in the match
expression, we obtain $2^{n}$ flattened match expressions. Then, we parse the
flattened expressions using an augmented version of the reference grammar. The
augmented grammar adds expansions “ ::= ’<’ ’A’ ’>’” for each nonterminal
A, and similarly extends the grammar with expansions for variable binders
“{<T> var}.” Due to ambiguities in the grammar, we might obtain multiple parse
trees even for flattened expressions; $\mathit{mexprTrees}$ returns all of
them, along with a mapping of bound variables to the positions of their
matches in the respective derivation trees. After parsing the match
expression, the function $\mathit{matchTrees}(t,t^{\prime},P)$ matches a
derivation tree $t$ against a result $(t^{\prime},P)$ from
$\mathit{mexprTrees}$, where $t^{\prime}$ is a parse tree and $P$ a mapping
from bound variables to positions in $t^{\prime}$. Figure 1 shows the
definition of $\mathit{mexprTrees}$. In the definition,

  * •

$l(t)$ is the label of the tree $t$;

  * •

all alternatives in the definition are *mutually exclusive* (the first
applicable one is applied);

  * •

by $\mathit{numc}(t)$ we denote the number of children of the derivation tree
$t$;

  * •

by $\mathit{child}(t,i)$ we denote the $i$-th child of t, starting with 1;

  * •

$P_{i}$ is computed from a mapping $P$ by discarding all paths in $P$ not
starting with $i$ and taking the _tail_ (discarding the first element) for all
other paths; and

  * •

we use standard set union notation $\bigcup_{i=1}^{n}\beta_{i}$ for combining
variable assignments $\beta_{i}$.

Let $T$ be the label of the root of tree $t$. We define

$\mathit{match}(t,\mathit{mexpr})\coloneqq\\\
\left(\bigcup_{(t^{\prime},P)\in\mathit{mexprTrees}(T,\mathit{mexpr})}\\{\mathit{matchTrees}(t,t^{\prime},P)\\}\right)\setminus\\{\bot\\}$

$\displaystyle\mathit{matchTrees}(t,t^{\prime},P):=\begin{cases}\bot&\text{if
}l(t)\neq{}l(t^{\prime})\vee(\mathit{numc}(t^{\prime})>0\wedge\\\
&\qquad\mathit{numc}(t)\neq\mathit{numc}(t^{\prime}))\\\
[v\mapsto{}t]&\text{if }P=[v\mapsto{}()]\text{ for some }v\\\ \bot&\text{if
}\mathit{matchTrees}(\mathit{child}(t,i),\mathit{child}(t^{\prime},i),P_{i})=\bot\\\
&\qquad\text{for any }i\in[1,\dots,\mathit{numc}(t)]\\\
\bigcup_{i=1}^{\mathit{numc}(t)}\Big{(}&\\\
\quad\mathit{matchTrees}\big{(}\mathit{child}(t,i),&\\\
\quad\hphantom{\mathit{match}\big{(}}\mathit{child}(t^{\prime},i),P_{i}\big{)}\Big{)}&\text{otherwise}\\\
\end{cases}$

Figure 1. Recursive Definition of $matchTrees$.

##  0\. LABEL:main-sec:input_generation

We provide a formalization of our ISLa constraint solver, including two
correctness theorems and proof sketches.

We formalize input generation for ISLa as a transition system between
_Conditioned Derivation Trees (CDTs)_ ${}\Phi\triangleright{}t{}$, where
$\Phi$ is a set of ISLa formulas (interpreted as a conjunction) and $t$ a
(possibly open) derivation tree. Intuitively, $\bigwedge\Phi$ constrains the
inputs represented by $t$, similarly as $\llbracket{\varphi}\rrbracket$
constrains the language of the grammar. To make this possible, we need to
relax the definition of ISLa formulas: Instead of free variables, formulas may
contain references to tree nodes which they are concerned about. To that end,
tree nodes are assigned unique, numeric identifiers, which may occur
everywhere in ISLa formulas where a free variable might occur (variables bound
by quantifiers may not be replaced with tree identifiers).

Consider, for example, the ISLa constraint

$\varphi=\text{{forall}}~{}{\langle\mathit{id}\rangle{}}~{}{\mathit{id}}~{}\text{{in}}~{}{\mathit{start}}\text{:}\,{\text{(=
(str.len $\mathit{id}$) 17)}}$

constraining the XML grammar in Figure LABEL:main-fig:xml-bnf in (Dominic
Steinhöfel and Zeller, 2022) to identifiers of length 17, where $\mathit{id}$
is a bound variable of type $\langle\mathit{ID}\rangle{}$ and $\mathit{start}$
is a free variable of type $\langle\mathit{start}\rangle{}$. Let $t$ be a tree
consisting of a single (root) node with identifier 1, and labeled with
$\langle\mathit{start}\rangle{}$. Then, $\llbracket{\varphi}\rrbracket$ is
identical to the strings represented by the CDT

${}\\{\text{{forall}}~{}{\langle\mathit{id}\rangle{}}~{}{\mathit{id}}~{}\text{{in}}~{}{\mathit{1}}\text{:}\,{\text{(=~{}(str.len~{}$\mathit{id}$)~{}17)}}\\}\triangleright{}t{}.$

Our CDT transition system relates an input CDT to a set of output CDTs. We
define two properties of such transitions: A transition is _precise_ if the
input represents _at most_ the set of all strings represented by all outputs
together; conversely, it is _complete_ if the input represents _at least_ the
set of all strings represented by all outputs. Precision is mandatory for the
ISLa producer, since we have to avoid generating system inputs which do not
satisfy the specified constraints.

To define the semantics of CDTs, we first define the closed trees represented
by (the language of) _open_ derivation trees. We need the concept of a _tree
substitution_ : The tree $t[v\mapsto{}t^{\prime}]$ results from
$t=(X,\leq_{V},\leq_{S})$ by replacing the subtree rooted in node $v\in{}X$ by
$t^{\prime}$, updating $X$, $\leq_{V}$ and $\leq_{S}$ accordingly.

###### Definition 0.1 (Semantics of Open Derivation Trees).

Let $t\in\mathcal{T}(G)$ be a derivation tree for a grammar $G=(N,T,P,S)$. We
define the set $\mathcal{T}(t)\subseteq\mathcal{T}(G)$ of closed derivation
trees represented by $t$ as

$\displaystyle\mathcal{T}(t)$ $\displaystyle\coloneqq\,$
$\displaystyle\big{\\{}t[l_{1}\mapsto{}t_{1}]\cdots[l_{k}\mapsto{}t_{k}]\;|$
$\displaystyle\quad{}\phantom{{\land\;}}l_{i}\in\mathit{leaves}(t)\land{}k=\left|\mathit{leaves}(t)\right|$
$\displaystyle\quad{}{\land\;}(\forall{}j,m\in 1\dots
k:l\neq{}m\rightarrow{}l_{j}\neq{}l_{m})$
$\displaystyle\quad{}{\land\;}n_{i}=\mathit{label}(t_{i})=\mathit{label}(l_{i})$
$\displaystyle\quad{}{\land\;}G_{n_{i}}=(N,T,P,n_{i})\land{}t_{i}\in\mathcal{T}(G_{n_{i}})\big{\\}}$

Observe that for the tree consisting of a single node labeled with the start
symbol $S$, $\mathcal{T}(t)$ is identical to $\mathcal{T}(S)$. Furthermore,
for any _closed_ tree $t^{\prime}$, it holds that
$\mathcal{T}(t^{\prime})=\\{t^{\prime}\\}$.

We re-use the validity judgment defined from Definition LABEL:main-
def:isla_validation in our paper (Dominic Steinhöfel and Zeller, 2022) for the
semantics definition for CDTs by interpreting tree identifiers in formulas
similarly to variables. Furthermore, the special variable assignment
$\beta_{t}$ for the derivation tree $t$ associates with each tree identifier
in $t$ the subtree rooted in the node with that identifier. Then, the
definition is a straightforward specialization of Definition 3.8 from (Dominic
Steinhöfel and Zeller, 2022):

###### Definition 0.2 (Semantics of CDTs).

Let $\Phi\subseteq 2^{\mathrm{Fml}}$ be a set of ISLa formulas for the
signature $\Sigma=(G,\mathrm{PSym},\mathrm{VSym})$, $t\in\mathcal{T}(G)$ be a
derivation tree, and $\pi$, $\sigma$ be interpretations for predicates and SMT
formulas. We define the semantics
$\llbracket{{}\Phi\triangleright{}t{}}\rrbracket$ of the CDT
${}\Phi\triangleright{}t{}$ as

$\llbracket{{}\Phi\triangleright{}t{}}\rrbracket\coloneqq\\{\mathit{str}(t^{\prime})\;|\;t^{\prime}\in\mathcal{T}(t)\land\mathit{closed}(t^{\prime})\land\pi,\sigma,\beta_{t^{\prime}}\models{}\bigwedge\Phi\\}.$

A CDT Transition System (CDTTS)CDT Transition System (CDTTS) is simply a
transition system between CDTs.

###### Definition 0.3 (CDT Transition System).

A _CDTTS_ for a signature $\Sigma=(G,\mathrm{PSym},\mathrm{VSym})$ is a
transition system $(C,\rightarrow)$, where, for $\Phi\in 2^{\mathrm{Fml}}$ and
$t\in\mathcal{T}(G)$, $C$ consists of CDTs ${}\Phi\triangleright{}t{}$, and
$\rightarrow\,\subseteq{}C\times{}C$. We write
$\mathit{cdt}\rightarrow\mathit{cdt^{\prime}}$ if
$(\mathit{cdt},\mathit{cdt^{\prime}})\in^{\prime}\,\rightarrow$.

Intuitively, one applies CDTTS transitions to an initial constraint with a
trivial tree only consisting of a root node labeled with the start
nonterminal, and collects “output” CDTs ${}\emptyset\triangleright{}t{}$ with
an empty constraint. The trees $t$ of such outputs are solutions to the
initial problem. We call a CDTTS _globally precise_ if all such trees $t$ are
actual solutions, i.e., the system does not produce wrong outputs; we call it
_globally complete_ if the entirety of trees $t$ from result CDTs represents
the full semantics of the input CDT.

###### Definition 0.4 (Global Precision and Completeness).

Let $(C,\rightarrow)$ be a CDTTS, and $R_{\mathit{cdt}}$ be the set of all
closed trees $t$ such that
$\mathit{cdt}\rightarrow\cdots\rightarrow{}\emptyset\triangleright{}t{}$ is a
derivation in $(C,\rightarrow)$. Then, $(C,\rightarrow)$ is _globally precise_
if, for each CDT $\mathit{cdt}$ in the domain of $\rightarrow$, it holds that
$\llbracket{\mathit{cdt}}\rrbracket\supseteq\\{\mathit{str}(t)|{}t\in{}R_{\mathit{cdt}}\\}$.
The CDTTS is _globally complete_ if it holds that
$\llbracket{\mathit{cdt}}\rrbracket\subseteq\\{\mathit{str}(t)|{}t\in{}R_{\mathit{cdt}}\\}$.

To enable transition-local reasoning about precision and completeness, we
define notions of local precision and completeness. Local precision is the
property that _at each transition step_ , no “wrong” inputs are added, and
local completeness the property that no transition step loses information.

###### Definition 0.5 (Local Precision and Completeness).

A CDTTS $(C,\rightarrow)$ is _precise_ if, for each CDT $\mathit{cdt}$ in the
domain of $\rightarrow$, it holds that
$\llbracket{\mathit{cdt}}\rrbracket\supseteq\bigcup_{\mathit{cdt}\rightarrow\mathit{cdt^{\prime}}}(\llbracket{\mathit{cdt^{\prime}}}\rrbracket)$.
The CDTTS is _complete_ if it holds that
$\llbracket{\mathit{cdt}}\rrbracket\subseteq\bigcup_{\mathit{cdt}\rightarrow\mathit{cdt^{\prime}}}(\llbracket{\mathit{cdt^{\prime}}}\rrbracket)$.

As for “soundness” in first-order logic (see, e.g., (van Dalen, 1994)), local
precision implies global precision, i.e., it suffices to show that the
individual transitions are precise to obtain the property for the whole
system. This is demonstrated by the following Lemma 0.6. Note that the
opposite direction does not hold, since a CDTTS could in theory lose precision
locally and recover it globally, although it is unclear how (and why) such a
system should be designed.

###### Lemma 0.6.

A locally precise CDTTS is also globally precise.

###### Proof.

The lemma trivially holds if $R_{\mathit{cdt}}=\emptyset$. Otherwise, let
$\mathit{cdt}_{0}\rightarrow\mathit{cdt_{1}}\rightarrow\cdots\rightarrow{}\emptyset\triangleright{}t{}$
be any transition chain s.t. $\mathit{cdt}_{0}=\mathit{cdt}$ and
$t\in{}R_{\mathit{cdt}}$. Then, it follows from local precision that
$\llbracket{\mathit{cdt}_{k}}\rrbracket\supseteq\llbracket{\mathit{cdt}_{k+1}}\rrbracket$
for $k=0,\dots,n-1$, and by transitivity of $\supseteq$ also
$\llbracket{\mathit{cdt}_{k}}\rrbracket\supseteq\llbracket{\mathit{cdt}_{l}}\rrbracket$
for $0\leq{}k<l\leq{}n$. Since
$\llbracket{{}\emptyset\triangleright{}t^{\prime}{}}\rrbracket=\mathit{str}(t^{\prime})$
for closed $t^{\prime}$, the lemma follows. ∎

Global completeness cannot easily be reduced to local completeness: It
includes the “termination” property that all derivations end in CDTs with
empty constraint set; furthermore, one has to show that there is an applicable
transition for each CDT with non-empty semantic.

Our ISLa solver prototype implements the CDTTS in Fig. 2. It solves SMT and
semantic predicate constraints by querying the SMT solver or the predicate
oracle, and eliminates existential constraints by inserting new subtrees into
the current conditioned tree. Only when the complete constraint has been
eliminated, we finish off the remaining incomplete tree by replacing open
leaves with suitable concrete subtrees. This is in principle a complete
procedure; yet, our implementation only considers a finite subset of all
solutions in solver queries and when performing tree insertion. Consequently,
it usually misses some solutions, but outputs _more diverse results more
quickly_ compared, e.g., to a naive search-based approach filtering out wrong
solutions.

(1)
$\displaystyle{{}\\{\dots,\varphi,\dots\\}\triangleright^{I}{t}{}\;\rightarrow\;\\{}{}\\{\dots,\varphi^{\prime}\dots\\}\triangleright^{I}{t}{}\;|\;$
$\displaystyle\hphantom{{}\\{\dots,\varphi,\dots\\}\triangleright^{I}{t}{}\;\rightarrow\;\\{}\quad\varphi^{\prime}\in\mathit{inv}(\varphi)\land\varphi\neq\varphi^{\prime}\\}\neq\emptyset$
(2)
$\displaystyle{}\Phi\triangleright^{I}{t}{}\;\rightarrow\;\\{{}\Phi\setminus\varphi\triangleright^{I}{t}{}\;|\;\varphi\in\Phi\cap\mathrm{PSym}_{\mathit{st}}\land\;\pi(\varphi)=\top\\}$
(3)
$\displaystyle{}\\{\dots,\text{{forall}}~{}{\text{int}}~{}{n}~{}\text{{in}}~{}{\varphi}\text{:}\,,\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\quad{}\\{\dots,\\{n\mapsto{}c\\}(\varphi),\dots\\}\triangleright^{I}{t}{}$
$\displaystyle\quad\text{where }c\in\mathrm{VSym}\text{ is \emph{fresh} and
}\mathit{vtype}(c)=\text{int}$ (4)
$\displaystyle{}\\{\dots,\overbrace{\text{{forall}}~{}{\mathit{type}}~{}{v}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi}}^{\psi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow\;\\{{}\\{\dots,\,\dots\\}\triangleright^{I}{t}{}\\}$
$\displaystyle\quad\text{if }\forall\text{ subrees }t^{\prime}\text{ of
}\mathcal{T}(\beta_{t}(\mathit{id})):$
$\displaystyle\quad\quad(\psi,t^{\prime})\in{}I\,\lor\mathit{label}(t^{\prime})\neq\mathit{type}$
(5)
$\displaystyle{}\\{\dots,\overbrace{\text{{forall}}~{}{\mathit{type}}~{}{v}\text{=}\text{``}\mathit{mexpr}\text{''}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi}}^{\psi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\\{{}\\{\dots,\,\dots\\}\triangleright^{I}{t}{}\\}\text{ if
}\forall\text{ subrees }t^{\prime}\text{ of
}\mathcal{T}(\beta_{t}(\mathit{id})):$
$\displaystyle\quad\quad\quad(\psi,t^{\prime})\in{}I\,\lor\mathit{label}(t^{\prime})\neq\mathit{type}\,\lor$
$\displaystyle\quad\quad\quad\text{there is no
}m=\mathit{match}(t^{\prime},\mathit{mexpr})$ (6)
$\displaystyle{}\\{\dots,\overbrace{\text{{forall}}~{}{\mathit{type}}~{}{v}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi}}^{\psi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\big{\\{}{}\\{\dots,\psi,\dots\\}\cup\bigcup\Psi\triangleright^{I\,\cup\,(\\{\psi\\}\times{}T)}{t}{}\big{\\}}~{}\mathrm{where}$
$\displaystyle\quad\quad\Psi=\big{\\{}\beta_{t}[v\mapsto{}t^{\prime}](\varphi)\;|\;t^{\prime}\in{}T\big{\\}}\,\land$
$\displaystyle\quad\quad{}T=\big{\\{}t^{\prime}\;|\;t^{\prime}=\beta_{t}(\mathit{id})\land(\psi,t^{\prime})\notin{}I\,\land$
$\displaystyle\quad\quad{}\hphantom{T=\big{\\{}t^{\prime}\;|\;}\mathit{label}(t^{\prime})=\mathit{type}\big{\\}}\neq\emptyset$
(7)
$\displaystyle{}\\{\dots,\overbrace{\text{{forall}}~{}{\mathit{type}}~{}{v}\text{=}\text{``}\mathit{mexpr}\text{''}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi}}^{\psi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\big{\\{}{}\\{\dots,\psi,\dots\\}\cup\bigcup\Psi\triangleright^{I\,\cup\,(\\{\psi\\}\times{}T)}{t}{}\big{\\}}~{}\mathrm{where}$
$\displaystyle\quad\quad\Psi=\big{\\{}\beta_{t}[v\mapsto{}t^{\prime}][m](\varphi)\;|\;(t^{\prime},m)\in{}T\big{\\}}\,\land$
$\displaystyle\quad\quad{}T=\big{\\{}(t^{\prime},m)\;|\;t^{\prime}=\beta_{t}(\mathit{id})\land(\psi,t^{\prime})\notin{}I\,\land$
$\displaystyle\quad\quad\quad{}\mathit{label}(t^{\prime})=\mathit{type}\;\land$
$\displaystyle\quad\quad\quad\text{there is an
}m=\mathit{match}(t,\mathit{mexpr})\big{\\}}\neq\emptyset$

(8)
$\displaystyle{}\Phi\triangleright^{I}{t}{}\;\rightarrow\;\\{{}\Phi\triangleright^{I}{t^{\prime}}{}\;|\;t^{\prime}\in\mathit{expand}^{\forall}_{\Phi}(t)\neq\emptyset\\}$
(9)
$\displaystyle{{}\Phi\triangleright^{I}{t}{}\;\rightarrow\;\\{}{}\Phi\setminus\varphi\triangleright^{I}{\beta(t)}{}\;|\;$
$\displaystyle\quad\quad\varphi\in\Phi\cap\mathrm{Trm}_{\mathit{bool}}(\mathrm{VSym})\land\beta\in\sigma(\varphi)\neq\bot\\}$
(10)
$\displaystyle{{}\Phi\triangleright^{I}{t}{}\;\rightarrow\;\\{}{}\Phi\setminus\varphi\triangleright^{I}{\beta(t)}{}\;|\;$
$\displaystyle\quad\quad\varphi\text{ is \emph{first}
}\varphi\in\Phi\cap\mathrm{PSym}_{\mathit{sem}}\land\beta\in\pi(\varphi)\notin\\{\bot,\circlearrowleft\\}\\}$
(11)
$\displaystyle{}\\{\dots,\overbrace{\text{{exists}}~{}{\mathit{type}}~{}{v}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi}}^{\psi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\bigcup_{\xi\in\Psi}\big{\\{}{}\\{\dots,\xi,\dots\\}\triangleright^{I}{t}{}\big{\\}}~{}\mathrm{where}$
$\displaystyle\quad\quad\Psi=\big{\\{}{\beta_{t}[v\mapsto{}t^{\prime}]}(\varphi)\;|\;t^{\prime}\in{}T\big{\\}}\,\land$
$\displaystyle\quad\quad{}T=\big{\\{}t^{\prime}\;|\;t^{\prime}=\beta_{t}(\mathit{id})\land(\psi,t^{\prime})\notin{}I\,\land$
$\displaystyle\quad\quad\quad{}\mathit{label}(t^{\prime})=\mathit{type}\,\big{\\}}\neq\emptyset$
(12)
$\displaystyle{}\\{\dots,\overbrace{\text{{exists}}~{}{\mathit{type}}~{}{v}\text{=}\text{``}\mathit{mexpr}\text{''}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi}}^{\psi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\bigcup_{\xi\in\Psi}\big{\\{}{}\\{\dots,\xi,\dots\\}\triangleright^{I}{t}{}\big{\\}}~{}\mathrm{where}$
$\displaystyle\quad\quad\Psi=\big{\\{}\beta_{t}[v\mapsto{}t^{\prime}][m](\varphi)\;|\;(t^{\prime},m)\in{}T\big{\\}}\,\land$
$\displaystyle\quad\quad{}T=\big{\\{}(t^{\prime},m)\;|\;t^{\prime}=\beta_{t}(\mathit{id})\land(\psi,t^{\prime})\notin{}I\,\land$
$\displaystyle\quad\quad\quad{}\mathit{label}(t^{\prime})=\mathit{type}\;\land$
$\displaystyle\quad\quad\quad\text{there is an
}m=\mathit{match}(t,\mathit{mexpr})\big{\\}}\neq\emptyset$ (13)
$\displaystyle{}\\{\dots,\text{{exists}}~{}{\mathit{type}}~{}{v}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\big{\\{}{}\\{\dots,\\{v\mapsto{}\mathit{nid}\\}(\varphi),\dots\\}\cup\Phi_{\mathit{orig}}\triangleright^{I}{\\{\mathit{id}\mapsto{}t^{\prime}\\}(t)}{}\;|$
$\displaystyle\quad\quad(\mathit{nid},t^{\prime})\in\mathit{insert}(\mathit{makeTree}(v),\beta_{t}(\mathit{id}))$
(14)
$\displaystyle{}\\{\dots,\text{{exists}}~{}{\mathit{type}}~{}{v}\text{=}\text{``}\mathit{mexpr}\text{''}~{}\text{{in}}~{}{\mathit{id}}\text{:}\,{\varphi},\dots\\}\triangleright^{I}{t}{}\;\rightarrow$
$\displaystyle\quad\big{\\{}{}\\{\dots,\\{v\mapsto{}\mathit{nid}\\}(\varphi),\dots\\}\cup\Phi_{\mathit{orig}}\triangleright^{I}{\\{\mathit{id}\mapsto{}t^{\prime}\\}(t)}{}\;|$
$\displaystyle\quad\quad(\mathit{nid},t^{\prime})\in\mathit{insert}(\mathit{makeTree}(v,\mathit{mexpr}),\beta_{t}(\mathit{id}))$
(15)
$\displaystyle{}\emptyset\triangleright^{I}{t}{}\;\rightarrow\;\\{{}\emptyset\triangleright^{I}{t^{\prime}}{}\;|\;t^{\prime}\in\mathcal{T}(t)\\}\neq\\{{}\emptyset\triangleright^{I}{t}{}\\}$
(16)
$\displaystyle{}\Phi\triangleright^{I}{t}{}\;\rightarrow\;\\{{}\Phi\triangleright^{I}{t^{\prime}}{}\;|\;t^{\prime}\in\mathcal{T}(t)\\}\neq\\{{}\Phi\triangleright^{I}{t}{}\\}$
$\displaystyle\quad\text{ if
}\Phi\subseteq\\{p(\dots)\;|\;p\in\mathrm{PSym}_{\mathit{sem}}\\}$

Figure 2. Efficient ISLa CDTTS Transition Relation

#### Transition Rules

In the ISLa CDTTS, we use _indexed_ CDTs ${}\Phi\triangleright^{I}{t}{}$. In
the index set $I$, we track previous matches of universal quantifiers to make
sure that we do not match the same trees over and over. Since SMT formulas can
now also contain variables, evaluating them can result in a _model_ $\beta$
(an assignment). Note that we can obtain different assignments by repeated
solver calls (negating previous solutions). We divide the set $\mathrm{PSym}$
of predicate symbols into two disjoint sets $\mathrm{PSym}_{\mathit{st}}$ and
$\mathrm{PSym}_{\mathit{sem}}$ of _structural_ and _semantic_ predicates.
Structural predicates address constraints such as _before_ or _within_ , and
they evaluate to $\top$ or $\bot$. _Semantic_ predicates formalize constraints
such as specific checksum implementations. They may additionally evaluate to a
set of assignments, as in the case of satisfiable SMT expressions, or to the
special value “not ready” (denoted by $\circlearrowleft$). Intuitively, an
evaluation results in $\top$ ($\bot$) if all of (not any of) the derivation
trees represented by an abstract tree satisfy the predicate. Assignments are
returned if the given tree can be completed or “fixed” to a satisfying
solution. One may obtain $\circlearrowleft$ if the constrained tree lacks
sufficient information for such a computation (e.g., the inputs of a checksum
predicate are not yet determined).

We explain the individual transition rules of the CDTTS from Fig. 2. Eq. 1
uses a function $\mathit{inv}:\mathrm{Fml}\rightarrow 2^{\mathrm{Fml}}$ to
enforce the invariant that all formulas $\varphi\in\Phi$ are in Negation
Normal Form (NNF) and do not contain top-level conjunctions and disjunctions.
Basically, $\mathit{inv}$ converts its input into Disjunctive Normal Form and
returns the disjunctive elements. It is only applicable to CDTs whose
constraints do not satisfy the invariant. Eq. 2 eliminates satisfied
structural predicate formulas from a constraint set. Existential quantifiers
over numbers are eliminated in Eq. 3 by introducing a fresh (not occurring in
the containing CDT) variable symbol with the special nonterminal type int for
natural numbers.

Eqs. 4 and 5 eliminate universal formulas that have already been matched with
all applicable subtrees, and which cannot possibly be matched against _any_
extension of the (open) tree. This is the case if the nonterminal type of the
quantified variable is not reachable from any leaf and, if there is a match
expression, the current tree cannot be completed to a matching one.

Universal formulas with and without match expressions are subject of Eqs. 6
and 7. First, matching subtrees of the tree $\beta_{t}(\mathit{id})$
identified with $\mathit{id}$ are collected in a set $T$. We only consider
subtrees that are not already matched, i.e., where $(\psi,t^{\prime})$ is not
yet in the index set $I$. If $T$ is empty, the rules are not applicable.
Otherwise, the set $\Phi$ of all instantiations of $\varphi$ according to the
discovered matches is added to the constraint set. We record the
instantiations $(\psi,t^{\prime})$, for all matched trees $t^{\prime}$, in the
index set. The output of these rules is a singleton.

If universal quantifiers remain which cannot be matched or eliminated, we
expand the current tree in Eq. 8. The function
$\mathit{expand}^{\forall}_{\Phi}(t)$ returns all possible trees $t^{\prime}$
in which each open leaf has been expanded _one step_ according to the grammar.
However, we only expand leaves which are bound by a universal quantifier, that
is, which represent possible subtrees that could be unified with a universally
quantified formula. For this reason, we pass $\Phi$ as an argument. We call
the remaining, unbound grammar symbols _free nonterminals_. For example, the
XML constraint in Listing LABEL:main-lst:xml_constraint from our paper
(Dominic Steinhöfel and Zeller, 2022) does not restrict the instantiation of
$\langle\mathit{text}\rangle{}$ nonterminals. Thus,
$\langle\mathit{text}\rangle{}$ is a free nonterminal which we will not expand
with Eq. 8. Instead, such nonterminals are instantiated to concrete closed
subtrees in a single step by Eqs. 15 and 16. In our implementation, we use a
standard coverage-based fuzzer to that end. Thus, we avoid producing many
strings which only differ, e.g., in identifier names or text passages within
XML tags.

Eqs. 9 and 10 eliminate _satisfiable_ SMT or semantic predicate formulas by
querying $\sigma$ or $\pi$ (there is no transition for unsatisfiable or “not
ready” formulas). The transition result consists of one instantiation per
returned assignment $\beta$.

The only remaining constraints—in satisfiable constraint sets— are existential
formulas, and semantic predicate formulas that are not yet ready to provide a
solution. Existential formulas can be matched just like universal ones; but
instead of returning one result with all matches, Eqs. 11 and 12 return a
_set_ of solutions with one match each.

In addition to matching, we provide two rules Eqs. 13 and 14 to eliminate
existential formulas using _tree insertion_. Note that, as exception to the
general principle that the rules in the CDTTS are mutually exclusive, we can
apply Eqs. 11 and 12 _and_ Eqs. 13 and 14 wherever possible. The insertion
routine $\mathit{insert}(\mathit{newTree},t,$) guarantees that all returned
results contain all nodes from the original tree $t$ as well as the complete
tree $\mathit{newTree}$. Nevertheless, tree insertion is an aggressive
operation that may violate constraints that were satisfied before. For this
reason, we have to add the original constraint
$\mathit{\Phi_{\mathit{orig}}}$, from which we started solving, again to the
constraint set; if the tree insertion did not violate structural constraints,
the original constraint can usually be quickly eliminated. However, tree
insertion can also entail the necessity of subsequent tree insertions, e.g.,
if a new identifier was added that needs to be declared. Our implemented
insertion routine prioritizes structurally simple solutions, for which this is
usually not necessary. In the appendix, we provide details on tree insertion.

Finally, Eqs. 15 and 16 “finish off” the remaining open derivation trees by
replacing all open leaves with suitable concrete subtrees. In the case of Eq.
15, this yields a decisive result of the CDTTS. Eq. 16 addresses residual “not
ready” semantic predicate formulas. We compute the represented closed subtrees
such that all information for evaluating the semantic predicates is present.
After this step, Eq. 10 must be applicable.

In the appendix, we argue for the correctness of the subsequent precision and
completeness theorems.

###### Theorem 0.7.

(Precision) The ISLa CDTTS in Fig. 2 is globally precise.

###### Proof Sketch..

By Lemma 0.6, we prove global precision by showing that each individual
transition rule is _locally_ precise, i.e., that the produced states do not
represent derivation trees that were not originally in the semantics of the
inputs CDT.

Eq. 1 is precise since conversion to Disjunctive Normal Form is equivalence-
preserving. Elimination of structural predicates (Eq. 2) is trivially precise
(removing a true element from a conjunction does not change the semantics).

Eqs. 4 and 5 are precise because a universal quantifier that does not match
any tree element evaluates to true according to Definition LABEL:main-
def:isla_validation in our paper (Dominic Steinhöfel and Zeller, 2022), and we
only remove it if we can be sure that no possible extension of an open tree
will ever match the quantifier. If a match is already in the index set, we can
be sure that it already has been considered due to the definition of Eqs. 6
and 7, which are the only rules ever adding to that set.

Eqs. 6 and 7 are precise because we only _add_ the matching instantiations of
the inner formula to the (conjunctive) constraint set.

Tree expansion (Eq. 8) is precise since by considering _more concrete_ trees,
the set of concrete trees represented by the input CDT is only ever
_decreased_ in the outputs (cf. Definition 0.1).

The elimination of SMT formulas (Eq. 9) is precise since their semantics is
defined via the interpretation function $\sigma$, which we query to produce
valid output states. The same holds for Eq. 10 for semantic predicates.

Existential quantifier matching (Eqs. 11 and 12) is precise since it conforms
to Definition LABEL:main-def:isla_validation in our paper (Dominic Steinhöfel
and Zeller, 2022) inasmuch it creates one instantiated CDT for each match in
the input CDT. The original formula is removed from these results, but the
instantiation retained.

The tree insertion rules (Eqs. 13 and 14) (the most complicated ones in our
system due to the complexity of tree tree insertion itself) are trivially to
prove, because we add the additional constraint again to the constraint set.

Finally, Eqs. 15 and 16 consider more concrete trees and are therefore precise
for the same reasons as Eq. 8. ∎

###### Theorem 0.8.

(Completeness) The ISLa CDTTS in Fig. 2 is globally complete.

###### Proof Sketch..

To prove the global completeness of our system, we have to show that the
semantics of each input CDT is contained in the semantics of all reachable
CDTs with empty constraint set. We reduce this problem as follows. First, we
show _local_ completeness, i.e., that no information is lost by applying any
transition rule of our CDTTS. Second, we argue that for each _valid_ CDT,
there is an applicable rule in the CDTTS. Third, we argue that for each input
CDT, there is _one_ output CDT which is _closer_ to a state with empty
constraint set in the CDTTS than the inputs. From this, we conclude global
completeness as follows: Since for each valid state, there is a transition
step from which get closer to an output state with empty constraint set, this
also holds for each valid state produced by this step. By additionally
requiring that the individual steps do not lose information, we conclude
global completeness.

We argue for the local completeness of a chosen set of CDTTS rules.

The expansion and finishing rules are locally complete if _all_ expansions are
considered. This is the case in our CDTTS, although our actual implementation
can only ever consider a finite set of solutions.

The same holds for solving SMT formulas. Note that if we only consider a
finite solution set as in our prototype, it is crucial that _there remain no
universal quantifiers_ in the constraint set. Otherwise, we could obtain
instantiations that conflict with formulas obtained from later quantifier
instantiation. This is not a problem in the theoretic framework, though, since
there we consider _all possible_ solutions, of which at least some will not
conflict with atoms nested in remaining universal quantifiers.

Tree insertion, which is easy to show precise, is more problematic to show
locally complete, since we add the original constraint set. However, since we
consider _all_ possible insertions, there have to be some satisfying that
constraint, since the input CDT is valid.

Since we defined one rule for each syntactic construct in ISLa, there is one
rule for each valid input state. Eq. 8, for example, only expands nonterminals
with potential concrete subtrees matching existing existential quantifiers;
for all other nonterminals, the finishing rules will be applicable.

The general measure to show that each transition produces a state that is
closer to an empty constraint set is the size of the constraint set together
with the nesting depth of contained quantifiers. If either of these measures
decreases in each step, we eventually reach an empty constraint set. That we
get closer to an empty constraint set is clear to see for all elimination
rules. In case of the matching rules, we reduce the complexity of the
constraint set by peeling off the outer quantifier. Again, tree insertion is
most problematic: It peels of the existential quantifier, but adds the
original constraint set. Here, it is important to see that there are some
insertions for which we can remove the existential constraint we eliminated by
tree insertion by _matching_ , and that we thus do not have to keep re-
inserting. ∎

We explain the main building blocks used in our ISLa CDTTS (Fig. 2) in more
detail.

#### Tracking Instantiations

Our CDTTS stepwise expands open trees and checks if existing universal
quantifiers match the expanded tree. Expansion does not eliminate a universal
quantifier, since it might apply to not yet generated subtrees. To avoid
endlessly instantiating universal quantifiers with the _same_ trees, we track
already performed universal quantifier instantiations. To that end, we augment
CDTs with an _index set_ $I$ consisting of pairs of universal formulas and
trees with which they already have been unified; we write
${}\Phi\triangleright^{I}{t}{}$ for the enhanced structures.

#### Invariant

We maintain the invariant that all formulas $\varphi\in\Phi$ in CDTTSs
${}\Phi\triangleright{}t{}$ are in NNF, i.e., negations only occur directly
before predicate formulas and within SMT expressions, and are free of
conjunctions and disjunctions (on top level; they are allowed inside of
quantifiers and within SMT formulas). The function
$\mathit{inv}:\mathrm{Fml}\rightarrow 2^{\mathrm{Fml}}$ first converts its
argument into NNF by pushing negations inside (e.g.,
$\text{{not}}~{}\text{{exists}}~{}{\mathit{type}}~{}{v}~{}\text{{in}}~{}{w}\text{:}\,{\varphi}$
gets
$\text{{forall}}~{}{\mathit{type}}~{}{v}~{}\text{{in}}~{}{w}\text{:}\,{\text{{not}}~{}\varphi}$,
and, for $\psi\in\mathrm{Trm}_{\mathit{bool}}(V)$, $\text{{not}}~{}\psi$ gets
$\text{(not $\psi$)}\in\mathrm{Trm}_{\mathit{bool}}(V)$). Then, it converts
the result into Disjunctive Normal Form by applying distributivity laws, which
yields a _set_ of disjunction-free formulas in NNF. Finally, it splits all
top-level conjunctions outside SMT expressions in the result set into multiple
formulas.

#### SMT Models

In Fig. 2, we apply the interpretation $\sigma$ for SMT expressions to Boolean
terms $\mathrm{Trm}_{\mathit{bool}}(V)$ with a non-empty variable set $V$,
i.e., the evaluated expressions may contain uninterpreted String constants. In
this case, the SMT solver will _either_ return $\bot$ in case of an
unsatisfiable constraint (or time out, which we interpret as $\bot$), _or_ an
assignment $\beta$ (a _model_). Since we can call the solver repeatedly and
ask for different solutions (by adding the negated previous solutions as
assumptions), we assume that we get a _set_ of assignments of tree identifiers
to new subtrees from $\sigma$.

#### Semantic Predicates

We divide the set $\mathrm{PSym}$ of predicate symbols into two disjoint sets
$\mathrm{PSym}_{\mathit{st}}$ and $\mathrm{PSym}_{\mathit{sem}}$ of
_structural_ and _semantic_ predicates. Structural predicates address
structural constraints, such as _before_ or _within_. They evaluate to $\top$
or $\bot$. _Semantic_ predicates formalize more complex constraints, such as
specific checksum implementations. In addition to $\top$ or $\bot$, semantic
predicate formulas may evaluate to a set of assignments, as in the case of
satisfiable SMT expressions, or to the special value “not ready” (denoted by
$\circlearrowleft$). Intuitively, an evaluation results in $\top$ ($\bot$) if
all of (not any of) the concrete derivation trees represented by an abstract
tree satisfy the predicate. A set of assignments is returned if there are
reasonable “fixes” of the tree (e.g., all elements relevant for a checksum
computation are determined, such that the checksum can be computed by the
predicate). One may obtain $\circlearrowleft$ if the constrained tree lacks
sufficient information for such a computation; for instance, we cannot compute
a checksum if the summarized fields are still abstract.

In contrast to all other constraint types, the _order of semantic predicate
formulas within a conjunction matters_ (we use ordered sets in the
implementation of our CDTs). The reason is that each semantic predicate comes
with its own, atomic solver. Consider, for example, a binary format which
requires a semantic predicate for the computation of a data field (e.g.,
requiring a specific compression algorithm) and another one for a checksum
which also includes the data field. Then, one must _first_ compute the value
of the data field, and _then_ the value of the checksum. Changing this order
would result in an invalid checksum. Since SMT formulas are composable, we
recommend using semantic predicates only if the necessary computation can
either not be expressed in SMT-LIB, or the solver frequently times out when
searching for solutions.

#### Tree Insertion

Existential constraints can occasionally be solved by matching them against
the indicated subtree, similarly to universal quantifiers. In general, though,
we have to manipulate the tree to enforce the existence of the formalized
structure. If a successful match is not possible, we therefore constructively
_insert_ a new tree into the existing one. The function $\mathit{makeTree}(v)$
creates a new derivation tree consisting of a single root node of type
$\mathit{vtype}(v)$. When passing it a match expression $\mathit{mexpr}$ as
additional argument, it creates a minimal open tree rooted in a node of type
$\mathit{label}(v)$ and matching $\mathit{mexpr}$. The function
$\mathit{insert}(t^{\prime},t)$ tries to inserts the tree $t^{\prime}$ into
$t$. Whether this is possible entirely depends on $t$, $t^{\prime}$ and the
grammar. In the simplest case, $t$ has an open leaf from which the nonterminal
$\mathit{label}(t^{\prime})$ is reachable. Then, we create a suitable tree
connecting the leaf and the root of $t^{\prime}$ and glue these components
together.

If this is not possible, we attempt to exploit recursive definitions in the
grammar. Consider, for example, a partial XML document according to the
grammar in Figure LABEL:main-fig:xml-bnf in our paper (Dominic Steinhöfel and
Zeller, 2022) and the constraint
$\text{{exists}}~{}{\langle\mathit{xml\text{-}open\text{-}tag}\rangle{}}~{}{\text{optag}}~{}\text{{in}}~{}{\text{tree}}\text{:}\,{\text{(=
optag "")}}$, where and tree points to a node with root of type
$\langle\mathit{xml\text{-}tree}\rangle{}$. If there is some opening tag of
form  in $\mathit{tree}$, we can eliminate the constraint. Otherwise, we
observe that the nonterminal $\langle\mathit{xml\text{-}tree}\rangle{}$ is
_reachable from itself_ in the grammar graph. Thus, we can replace an existing
$\langle\mathit{xml\text{-}tree}\rangle{}$ node in $\mathit{tree}$ by a number
of possible alternatives, comprising
$\text{}\,\langle\mathit{xml\text{-}tree}\rangle{}\allowbreak\langle\mathit{xml\text{-}close\text{-}tag}\rangle{}$,
which allows to insert both the already existing
$\langle\mathit{xml\text{-}tree}\rangle{}$ and the new opening tag  into
the expanded result.

#### Cost Function

The choice of the right cost function is crucial for the performance of the
solver, both in terms of generation speed (number of outputs per time) and
output diversity (e.g., creation of deep nestings in the case of XML, or
coverage of combinations of language constructs in the case of C).

Our cost function computes the weighted geometric mean of _cost factors_
$\mathit{cf}_{i}$ and corresponding _weights_ $w_{i}$ as

$\mathit{cost}=\left(\prod_{i=1,\dots,n}^{w_{i}\neq
0}(\mathit{cf}_{i}+1)^{w_{i}}\right)^{\left(\sum_{i=1,\dots,n}^{w_{i}\neq
0}w_{i}\right)^{-1}}-1$

We filter out pairs of cost factors and weights where the weight is 0; in this
case, the corresponding cost factor is deactivated. Furthermore, we avoid the
case that the final cost value is 0 if one of the factors is 0 by incrementing
each factor by 1, and finally decrementing the result by 1 again.

We chose the following cost factors:

Tree closing cost.:

We precompute, for each nonterminal in the grammar, an approximation of the
instantiation effort of that nonterminal, roughly by instantiating it several
times randomly with a fuzzer, and then summing up the sizes of the possible
grammar expansion alternatives in the resulting tree. The closing cost for a
derivation tree is defined as the sum of the costs of each nonterminal symbol
in all open leaves of the tree.

Constraint cost.:

Certain constraints are more expensive to solve than others. In particular,
solving existential quantifiers by tree insertion is computationally costly.
This cost factor assigns higher cost for constraints with existential and
deeply nested quantifiers.

Derivation depth penalty.:

As the solver’s queue fills up, it becomes more improbable for individual
queue elements to be selected next. If we assign a cost to the derivation
depth, it becomes more likely that the solver eventually comes back to partial
solutions discovered earlier, avoiding starvation of such inputs.

k-path coverage.:

When choosing between different partial trees, we generally want to generate
those exercising more language features at once. The k-path coverage metric
(Havrikov and Zeller, 2019) computes all paths of length k in a grammar and
derivation tree; the proportion of such paths covered by a tree is then the
coverage value. We penalize trees which cover only few k-paths. The concrete
value of k is configurable; the default is 3.

Global k-path coverage.:

For each final result produced by the solver, we record the covered k-paths
and from then on prefer solutions covering _additional_ language features.
Once all k-paths in a grammar have been covered, we erase the record.

The influence of these cost factors can be controlled by passing a tuple of
weights to the solver. We provide a reasonable default vector
($(11,3,5,20,10)$), but in certain cases, a problem-specific tuning might be
necessary to improve the performance. Our implementation provides an
evolutionary parameter tuning mechanism, which runs the solver with randomly
chosen weights, and then computes several generations of weight vectors using
crossover and mutation. The fitness value of a weight vector is determined by
the generation speed, a vacuity estimator, and a k-path-based coverage
measure.

##  0\. LABEL:main-sec:evaluation

0.[]

###  0.0. LABEL:main-sub:rq3_islearn

In the subsequent LABEL:lst:islearn_constraint_dot to
LABEL:lst:islearn_constraint_icmp_echo_checksum, we list the constraints that
ISLearn mined in our case study for our third research question.

⬇

((forall <graph_type> container in start:

exists <DIGRAPH> elem in container:

(= elem "digraph") or

forall <edge_stmt> container_0 in start:

exists <edgeop> elem_0 in container_0:

(= elem_0 "--")) and

(forall <graph> container_1 in start:

exists <GRAPH> elem_1 in container_1:

(= elem_1 "graph") or

forall <edge_stmt> container_2 in start:

exists <edgeop> elem_2 in container_2:

(= elem_2 "->")))

Listing 1: Constraint mined by ISLearn for DOT

⬇

(forall <expr> attribute=

"<maybe_comments><MWSS>{<name> prefix_use}" in start:

((= prefix_use "sqrt") or

(= prefix_use "string-append") or

$\dots$ or

exists <definition> outer_tag="(<MWSS>define<MWSS>(<MWSS><name>{<WSS_NAMES>
cont_attribute}<MWSS>)<MWSS><expr><MWSS>)"

in start:

(inside(attribute, outer_tag) and

exists <NAME> def_attribute="{<NAME_CHARS> prefix_def}" in cont_attribute:

(= prefix_use prefix_def))))

Listing 2: Constraint mined by ISLearn for Racket based on the XML _def-use_
pattern for prefixes in attributes

⬇

(forall <expr> use_ctx="<maybe_comments><MWSS>(<MWSS>{<name>
use}<wss_exprs><MWSS>)" in start:

((= use "sqrt") or

(= use "string-append") or

$\dots$ or

exists <definition> def_ctx=

"(<MWSS>define<MWSS>(<MWSS>{<name> def}<WSS_NAMES><MWSS>)<MWSS><expr><MWSS>)"
in start:

((before(def_ctx, use_ctx) and

(= use def))))) and

(forall <expr> attribute=

"<maybe_comments><MWSS>{<name> prefix_use}" in start:

((= prefix_use "sqrt") or

(= prefix_use "string-append") or

$\dots$ or

exists <definition> outer_tag="(<MWSS>define<MWSS>(<MWSS><name>{<WSS_NAMES>
cont_attribute}<MWSS>)<MWSS><expr><MWSS>)" in start:

(inside(attribute, outer_tag) and

exists <NAME> def_attribute="{<NAME_CHARS> prefix_def}" in cont_attribute:

(= prefix_use prefix_def))))

Listing 3: Racket constraint based on the XML _def-use_ pattern in addition to
an extended reST _def-use_ pattern

⬇

(forall <icmp_message> container in start:

exists <type> elem in container:

(= elem "00 ") or

forall <icmp_message> container_0 in start:

exists <type> elem_0 in container_0:

(= elem_0 "08 ")))

Listing 4: ISLearn constraint for ICMP Echo type fields

⬇

((forall <icmp_message> container in start:

exists <type> elem in container:

(= elem "00 ") or

forall <icmp_message> container_0 in start:

exists <type> elem_0 in container_0:

(= elem_0 "08 ")))) and

forall <icmp_message> container in start:

exists <checksum> checksum in container:

internet_checksum(container, checksum)

Listing 5: Constraint learned by ISLearn for ICMP Echo after adding a
predicate for Internet Checksums

## References

  * (1)
  * Havrikov and Zeller (2019) Nikolas Havrikov and Andreas Zeller. 2019.  Systematically Covering Input Structure. In _34th IEEE/ACM International Conference on Automated Software Engineering (ASE)_. IEEE, 189–199.  https://doi.org/10.1109/ASE.2019.00027
  * Steinhöfel (2022) Dominic Steinhöfel. 2022\.  The ISLa Language Specification.  https://rindphi.github.io/isla/islaspec/ Accessed: 2022-08-23.
  * Dominic Steinhöfel and Zeller (2022) Dominic Steinhöfel and Andreas Zeller. 2022.  Input Invariants. In _Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’22), November 14–18, 2022, Singapore_. ACM.  To appear..
  * van Dalen (1994) Dirk van Dalen. 1994\.  _Logic and Structure (3rd ed.)_.  Springer.