# TTPXHunter: Actionable Threat Intelligence Extraction as TTPs from Finished
Cyber Threat Reports

Nanda Rani1, Bikash Saha1, Vikas Maurya1, Sandeep Kumar Shukla1
1Department of Computer Science and Engineering, Indian Institute of
Technology Kanpur,
Kanpur, India
<EMAIL_ADDRESS>
###### Abstract

Understanding the modus operandi of adversaries aids organizations to employ
efficient defensive strategies and share intelligence in the community. This
knowledge is often present in unstructured natural language text within threat
analysis reports. A translation tool is needed to interpret the modus operandi
explained in the sentences of the threat report and convert it into a
structured format. This research introduces a methodology named TTPXHunter for
automated extraction of threat intelligence in terms of Tactics, Techniques,
and Procedures (TTPs) from finished cyber threat reports. It leverages cyber
domain-specific state-of-the-art natural language model to augment sentences
for minority class TTPs and refine pinpointing the TTPs in threat analysis
reports significantly. We create two datasets: an augmented sentence-TTP
dataset of $39,296$ sentence samples and a $149$ real-world cyber threat
intelligence report-to-TTP dataset. Further, we evaluate TTPXHunter on the
augmented sentence and report datasets. The TTPXHunter achieves the highest
performance of $92.42\%$ f1-score on the augmented dataset, and it also
outperforms existing state-of-the-art TTP extraction method by achieving an
f1-score of $97.09\%$ when evaluated over the report dataset. TTPXHunter
significantly improves cybersecurity threat intelligence by offering quick,
actionable insights into attacker behaviors. This advancement automates threat
intelligence analysis and provides a crucial tool for cybersecurity
professionals to combat cyber threats.

###### Index Terms:

Threat Intelligence, TTP Extraction, MITRE ATT&CK, Natural Language
Processing, Domain-specific Language model, TTP Classification, Cybersecurity

##  I Introduction

In the ever-evolving landscape of cybersecurity, Advanced Persistent Threats
(APTs) represent a significant challenge to worldwide security. Countering
APTs requires the development of sophisticated measures, which depend on the
detailed extraction and analysis of threat intelligence related to APTs [24,
27, 31]. It involves delving into the attacker’s modus operandi in terms of
Tactics, Techniques, and Procedures (TTPs) 111Categorized in the MITRE ATT&CK
Framework [7] explained in the threat reports, blogs, bulletins released by
security firms [1, 23]. These reports, written in unstructured natural
language, describe cyber adversaries’ modus operandi. Converting this
information into a machine-readable structured format improves threat
intelligence efforts and is crucial for comprehending and mitigating potential
threats [30].

Extracting TTPs from such reports is also crucial for recommending defensive
mechanisms. However, this process often encounters challenges, including a
lack of publicly available structured data, difficulties posed by polymorphic
words, and the challenge of interpreting the contextual meanings of sentences
present in the threat report and mapping them to MITRE ATT&CK (Adversarial
Tactics, Techniques, and Common Knowledge) TTP [2, 25]. We combat these
challenges in one of our previous works, which presents a TTP extraction tool
named TTPHunter [2]. It can automatically identify and catalog TTPs with the
f1-score of $0.88$ [2]. TTPHunter focused on the top 50 TTPs in the ATT&CK
framework because of the limited data availability for the remainder of the
TTP class. The remainder of the TTPs are particularly those that are either
newly emerging or less commonly used. This gap undermines the effectiveness of
TTPHunter, as incomplete TTP intelligence can lead to a reactive rather than
proactive security posture. Addressing this gap by advancing TTPHunter is
crucial to ensure that threat intelligence is exhaustive and reflects the
diverse adversarial tactics.

TABLE I: Notations and their Description Notation |  Description
---|---
$S_{i}$ |  $i^{th}$ sentence present in the report
$w_{i}$ |  $i^{th}$ word in the sentence
$n$ |  No. of sentences present in the report
$Aug\\_S$ |  List of augmented sentences for the sentence $S$
$\theta$ |  Threshold to choose relevant sentences
$S_{embed}$ |  Embedding vector for sentence $S$
$Top\\_5$ |  Top-5 selected words to create augmented sentence
$f(.)$ |  Embedding function
$\mathcal{M}$ |  Fine-tuned classifier
$v$ |  Feature vector
$t_{i}$ |  Predicted TTP class for $i^{th}$ sentence in the report
$\Theta$ |  Threshold to filter irrelevant sentences from threat report
$SCORE$ |  Similarity score between augmented and original sentence
$\hat{y}$ |  True label multi-hot vector for given threat report
$y$ |  Predicted label multi-hot vector for given threat report
$HL$ |  Hamming Loss
$\mathcal{R}$ |  A threat report which consists of $n$ sentences $(S)$
$\mathcal{T}$ |  Set of unique TTPs present in the database
$m$ |  No. of total unique TTPs present in the database
$\hat{\mathcal{T}}$ |  Predicted set of TTPs
$d$ |  No. of words present in the sentence

Therefore, this study presents TTPXHunter, an extended version of TTPHunter
[2], which meticulously refines and expands to recognize an impressive array
of $193$ TTPs. We address the limited data problem of TTPHunter by introducing
an advanced data augmentation method. This method meticulously preserves
contextual integrity and enriches our training dataset with additional
examples for emerging and less commonly used TTPs. Moreover, we also employ a
domain-specific language model that is finely tuned to grasp the nuanced,
context-driven meanings within this domain and enhance both the augmentation
process and the TTP classification. Further, we also enable TTPXHunter to
convert the extracted TTPs into the machine-readable format, i.e., STIX, which
facilitates the automated exchange, easier analysis, and integration across
different security tools and platforms [18, 34]. This advancement
significantly broadens the scope of threat intelligence gleaned from threat
reports and offers deeper insights into the TTPs employed by cyber adversaries
in APT campaigns. By extending TTPHunter’s extraction capabilities, this
research contributes to the critical task of threat intelligence gathering,
providing security analysts and practitioners with a more comprehensive
toolset for identifying, understanding, and countering APTs. The notations and
their descriptions used to explain the methodology are listed in Table. I.

TTPXHunter applies to a threat report denoted as $\mathcal{R}$ and extracts
set of TTPs denoted as $\hat{\mathcal{T}}$ explained within the report, where
$\hat{\mathcal{T}}\subseteq\mathcal{T}$ and
$\mathcal{T}=\\{t_{1},t_{2},t_{3},\ldots,t_{m}\\}$ which denotes a set of
target labels having $m$ number of TTPs. The methodology initiates with the
transformation of sentences segmented from threat report, denoted as
$\mathcal{R}=\\{S_{1},S_{2},\ldots,S_{n}\\}$; $n$ represents the number of
sentences in the report, into a high-dimensional feature space, i.e.,
$768$-dimension. This transformation, achieved through a cyber domain-specific
embedding function $f(.)$, maps each segmented sentence $S_{i}$ to a
$768$-dimension feature vector $v_{i}$ as

$v_{i}=\\{f(S_{i})\text{ };\quad\forall S_{i}\in\mathcal{R}\\}$

The embedding function encapsulates cybersecurity language’s rich semantic and
syntactic properties and the stage for nuanced inference. TTPXHunter exhibits
an inferential capability to predict a specific TTP for each segmented
sentence based on its embedded feature vector:

$t_{i}=\mathcal{M}(v_{i});\quad t_{i}\in\mathcal{T}$

Where $t_{i}$ represents the predicted TTP class for the feature vector
$v_{i}$, and $\mathcal{M}$ embodies the fine-tuned classification model that
aids in understanding the complex relationship between the features of the
segmented sentence and the TTP class. Further, the TTP extraction from the
threat report $\mathcal{R}$ is performed as:

$\hat{\mathcal{T}}=\bigcup_{i=1}^{n}t_{i}$

Our key contributions to this research are the following:

  * •

We introduce TTPXHunter222We plan to include the source code link in the
camera-ready version., an extended version of TTPHunter [2], which extracts
TTPs from threat intelligence reports using the SecureBERT [3] language model.
We fine-tune the model on our prepared augmented sentence-TTP dataset and
convert the extracted TTPs into structured and machine-readable STIX format.

  * •

We introduce a data augmentation method that utilizes the cyber-domain-
specific language model. This approach creates sentences related to TTPs by
preserving their contextual meaning while preparing new and varied sentences.

  * •

By leveraging the presented data augmentation method, we build an augmented
sentence-TTP dataset using the TTPHunter dataset prepared from the MITRE
ATT&CK knowledgebase. We build the augmented dataset using the MLM (Masked
Language Model) feature of the contextual natural language model, and it
extends samples from $10,906$ sentences to $39,296$ sentences covering $193$
ATT&CK TTPs.

  * •

We perform an extensive evaluation to measure the efficiency of TTPXHunter
over two different types of datasets: The augmented sentence dataset and the
Threat report dataset. We manually label $149$ real-word threat reports for
the report dataset.

The remainder of the paper is structured as follows: Section II discusses the
current literature, Section III presents the required background, Section IV
discusses presented TTPXHunter method, Section V demonstrate the experiment
done and evaluate the obtained results, Section VI presents the limitation in
proposed method along with it is possible future direction and Section VII
concludes this research contribution.

##  II Related Work

TABLE II: TTP Extraction Methods Comparison Research Work |  Year |  Extraction Technique |  Sentence Context-aware |  Identify Relevant Text |  STIX Support |  Domain-specific Capability |  Range of MITRE ATT&CK TTPs
---|---|---|---|---|---|---|---
Husari et al. [5] |  $2017$ |  TF-IDF, Ontology-based, and improved BM25 similarity rank |  $\times$ |  $\checkmark$ |  $\checkmark$ |  $\checkmark$ |  All TTPs
Legoy et al. [10] \- rcATT |  $2020$ |  TF-IDF and ML Models (KNN, Decision Tree, Random Forest, and Extra Tree) |  $\times$ |  $\times$ |  $\checkmark$ |  $\times$ |  All TTPs
Li et al. [6] \- AttacKG |  $2022$ |  Entity-based dependency graph and Graph-alignment algorithm |  $\times$ |  $\checkmark$ |  $\times$ |  $\checkmark$ |  All TTPs
Rani et al. [2] \- TTPHunter. |  $2023$ |  BERT/RoBERTa followed by Linear Classifier |  $\checkmark$ |  $\checkmark$ |  $\times$ |  $\times$ |  50 most frequently used TTPs only
Alam et al. [4] \- LADDER |  $2023$ |  Extract attack phases using a sequence tagging model and map these patterns to TTP using cosine similarity |  $\checkmark$ |  $\checkmark$ |  $\times$ |  $\times$ |  All TTPs
TRAM [8] |  $2023$ |  SciBERT followed by Linear Classifier |  $\checkmark$ |  $\times$ |  $\times$ |  $\times$ |  50 most frequently used TTPs only
TTPXHunter (Proposed) |  $2024$ |  Domain-specific SecureBERT with Linear Classifier |  $\checkmark$ |  $\checkmark$ |  $\checkmark$ |  $\checkmark$ |  All TTPs

Research on TTP extraction from threat intelligence reports is widely based on
ontology, graphs, and keyword-phrase matching methods [25, 2].

Initially, Husari et al. [5] present TTPDrill, which extracts threat actions
based on ontology and matches TTP’s knowledge base with extracted threat
action using the BM25 matching technique. Legoy et al. [10] present rcATT, a
classification tool based on Machine Learning (ML) algorithms. They use Term
Frequency–Inverse Document Frequency (TF-IDF) to prepare the dataset and
perform multi-class classification for target labels as TTP. The rcATT is
based only on sentence keywords, as TF-IDF ignores the sentence’s word
sequence and context. The model may fail when synonym words are present and
polymorphic nature words (the same words have a different meaning in a
different context). Li. et al. [6] introduce AttacKG, a graph template
matching technique. The method obtains IOCs and constructs entity-based
dependency graphs for every TTP present in ATT&CK by leveraging descriptions
on the MITRE website and matching them with the TTP’s templates prepared from
MITRE website data. To match the templates, they use the graph alignment
algorithm. AttacKG struggles to capture techniques identified by adjectives
(properties of IOCs) present in the sentences rather than verbs (threat
actions), such as masqueraded identity and obfuscated malware. Alam et al. [4]
introduce LADDER, a framework designed to enhance cyber threat intelligence
(CTI) by extracting and analyzing attack patterns from CTI reports, addressing
the limitations of traditional CTI that focuses on static indicators like IP
addresses. LADDER contains a subpart named TTPClassifier, which is structured
into three key steps: identifying sentences with attack pattern descriptions
using a binary classification model, pinpointing and extracting these attack
phrases with a sequence tagging model, and finally, mapping these patterns to
TTP IDs via cosine similarity method. To deal with the polymorphic nature of
words and leverage contextual information in the report sentences, Rani et al.
[2] present TTPHunter. This tool leverages the language models BERT and
RoBERTa to understand the context of the sentences present in the dataset and
map it to the correct TTP ID present in the dataset. Due to a dearth of
sentence datasets for many TTPs, TTPHunter is trained for only $50$ sets of
TTPs and has yet to map the full spectrum of TTPs present in the MITRE
knowledge base. After that, MITRE also introduced a TTP extraction tool named
TRAM (Threat Report ATT&CK Mapping) [8]. It is based on the scientific BERT
model, named SciBERT [22], a fine-tuned BERT model on a collection of
scientific reports.

In this paper, we extend our recent work TTPHunter [2] to extract TTPs present
in the collected threat report. The TTPHunter is fine-tuned on traditional
BERT and RoBERTa models, whereas we fine-tune cyber-domain-specific language
models to identify TTPs. Aghaei et al. [3] show that the cyber-domain-specific
language model can perform better than the traditional model trained on
general English sentences. Domain-specific words such as Windows and registry
have different meanings regarding general and cybersecurity usage. In
addition, we solve the limited dataset problem pointed out by [2] using the
data augmentation method. Our proposed method can extract the full spectrum of
TTPs in the MITRE ATT&CK knowledgebase. A comparison of our proposed model
TTPXHunter with the literature is shown in Table II.

##  III Background

This section presents the details of every framework, tool, and method used to
get insight into their background, which is required to understand the
methodology.

Figure 1: TTPXHunter Architecture

###  III-A MITRE ATT&CK Framework

The MITRE ATT&CK (Adversarial Tactics, Techniques, and Common Knowledge)
Framework [7] is a globally acknowledged comprehensive knowledge base designed
to understand cyber threats and adversary behaviors across different stages of
a cyber attack. It introduces a standardized lexicon and framework for the
classification and detailed description of attackers’ tactics, techniques, and
procedures (TTPs). The ATT&CK framework comprises three primary components:
Tactics, Techniques, and Procedures. Tactics represent the objectives or goals
adversaries aim to achieve throughout an attack, encompassing $14$ distinct
categories such as Reconnaissance, Resource Development, Initial Access,
Execution, and others [7]. Techniques detail the specific methods adversaries
employ to fulfill these tactics, each with a unique identifier and a
comprehensive description. Examples include phishing, password spraying,
remote code execution, and PowerShell exploitation. Procedures delve into the
detailed execution of techniques by attackers to achieve their tactical
objectives, illustrating how specific methods are applied in practice, such as
deploying a spearphishing email with malicious attachments to achieve initial
access. Beyond cataloging techniques, the ATT&CK framework maps real-world
attack scenarios to known techniques that enable organizations to understand
better how adversaries navigate through the stages of an attack. This
knowledge fosters the development of proactive defenses and offensive security
practices, enhances incident response efforts, and enriches threat
intelligence [23, 32].

###  III-B BERT Language Model

The natural language model plays a vital role in cyber threat intelligence,
particularly in extracting threat intelligence from natural language
cybersecurity texts. Among the popular language models, BERT (Bidirectional
Encoder Representations from Transformers) [14] holds significant importance
in tasks such as extracting threat intelligence, classifying threat data, NER
(Name Entity Recognition), detecting spam and phishing attacks [3, 17, 15].
BERT comprises a 12-layer stacked encoder part of the transformer, which
generates contextualized embeddings for natural language inputs. The training
of the BERT model involves two key components: Masked Language Model (MLM) and
Next Sentence Prediction (NSP). In the MLM, random words within a sentence are
masked, and the model learns to predict the masked word based on the context
of surrounding words present in the sentence. The NSP focuses on understanding
the context and meaning of a sentence by predicting the likelihood of the next
sentence in a given pair of sentences. Both tasks demonstrate the BERT model’s
ability to grasp the contextual understanding of sentences and capture the
relationships between words within a sentence. The BERT model’s proficiency in
understanding sentence context and word relationships makes it valuable for
various downstream tasks in cyber threat intelligence.

###  III-C TTPHunter

Our recent tool, TTPHunter [2], leverages the power of the language model BERT
to extract threat intelligence in the form of TTPs from natural language
threat report texts. The authors of TTPHunter fine-tune a pre-trained BERT
model using a sentence-TTP dataset collected from the MITRE knowledge base to
let the model understand the context of TTPs present in the MITRE ATT&CK
matrix and map a given sentence to relevant TTPs. One noteworthy feature of
TTPHunter is its ability to discern the significance of sentences. Rather than
indiscriminately mapping all sentences from a threat report, TTPHunter
selectively identifies and considers only those sentences that truly explain
TTPs, disregarding irrelevant information. To achieve this, we implement a
filtering mechanism on the model’s predicted probabilities. Our experiments
discovered that sentences with a probability higher than $0.64$ are relevant,
while those below the threshold were considered irrelevant. We adopt the same
threshold for identifying relevant sentences by TTPXHunter.

##  IV Proposed Methodology: TTPXHunter

Algorithm 1 Data Augmentation Algorithm

Input: $S\leftarrow[w_{1},w_{2},\dots,w_{d}]$ $\triangleright$ Input Sentence
consisting $d-$words
Output: $Aug\\_S$ $\triangleright$ List of augmented sentences for the input
sentence

1:$Aug\\_S\leftarrow[\;]$

2:for $i=1$ to $d$ do

3: $S^{\prime}\leftarrow S$

4: $S^{\prime}[i]\leftarrow<mask>$ $\triangleright$ Mask the $i^{th}$ word in
sentence S

5: $Predicted\\_words\leftarrow\textsc{SecureBERTMLM}(S^{\prime})$
$\triangleright$ Predict probable word using MLM

6: $Top\\_5\leftarrow\textsc{Select\\_top\\_5}(Predicted\\_words)$
$\triangleright$ Select top-5 probable words based on their probabilities

7: for $word$ in Top_5 do

8: $S^{\prime}[i]\leftarrow word$ $\triangleright$ Augmented sentence obtained
by replacing masked token

9: $SCORE\leftarrow\textsc{Cosine\\_Similarity}(S,S^{\prime})$

10: if $SCORE\geq\theta$ then

11: $Aug\\_S\leftarrow Aug\\_S\cup S^{\prime}$ $\triangleright$ Append
augmented sentence to output list

12: end if

13: end for

14:end for

15:Return $Aug\\_S$

16:function Cosine_Similarity($S,S^{\prime}$)

17: $S_{embed}\leftarrow\textsc{Sentence\\_Transformer}(S)$

18: $S^{\prime}_{embed}\leftarrow\textsc{Sentence\\_Transformer}(S^{\prime})$

19: Return $cosine(S_{embed},S^{\prime}_{embed})$

20:end function

In this study, we introduce TTPXHunter, an extended version of TTPHunter,
designed to overcome the challenges of limited data for less commonly
encountered TTPs and improve the performance of TTPHunter. It incorporates a
novel methodology encompassing data augmentation and domain-specific language
models to enhance the performance of TTP classification. The notations used to
explain the methodology are listed in Table. I.

TTPXHunter follows the idea used in TTPHunter of leveraging the natural
language model to extract TTPs from threat reports. TTPHunter is based on the
model, which is fine-tuned on general English sentences. The model trained on
general sentences can mislead the contextual embedding for domain-specific
words having different contexts comparatively. Cyber domain-specific words
such as Windows and Registry have entirely different meanings in the cyber
domain. Hence, we observe the need for a TTP extraction tool based on domain-
specific language models to provide more accurate contextual embeddings. To
fill this gap of domain-specific knowledge, we leverage the SecureBERT [3] to
fine-tune the proposed TTPXHunter and map sentences to the relevant TTPs they
represent. TTPXHunter incorporates a filtration mechanism to identify and
exclude irrelevant sentences from the TTP extraction results obtained from the
threat reports. The filtering mechanism ensures the model extracts the most
pertinent and meaningful TTPs for further analysis and discards unrelated
sentences. The overview and architecture of TTPXHunter are shown in Fig. 1.

The TTPHunter [2] is limited to $50$ prominent TTPs only out of $193$ TTPs due
to the limited sentence in the database for the remainder of the TTP class,
which results in incomplete or limited threat intelligence. Enhancing its
extraction capabilities is crucial for developing comprehensive and proactive
security strategies by leveraging the full spectrum of threat intelligence.
Therefore, we address this problem by presenting a data augmentation method in
TTPXHunter. This method creates more samples for the minority TTP class.

###  IV-A Contextual Data Augmentation

TABLE III: IOC Replacement

Base Name | Example Pattern |  Regex
---|---|---
Registry | HKEY_LOCAL_MACHINE\XXX\XXX\XX\Run |  (HKEY_LOCAL_MACHINE|HKEY_CURRENT_USER|HKEY_CLASSES_ROOT|HKEY_USERS|HKEY_CURRENT_CONFIG)\\\\(?:[^\\\\]+\\\\)*[^\\\\]+
Email |<EMAIL_ADDRESS>|  [a-zA-Z0-9._%\\+-]+@[a-zA-Z0-9.-]+\\.[a-zA-Z]{2,}
IP Address | 00.00.00.00 |  (\d{1,3}\\.){3}\d{1,3}
Domain | www.domain.com |  [a-zA-Z0-9.-]+\\.[a-zA-Z]{2,}
File Path | C:\XXX\yy |  ([a-zA-Z]:\\\\)?(?:[a-zA-Z0-9_-]+\\\\)*[a-zA-Z0-9_-]+\\.[a-zA-Z0-9_]+
File Name | file.exe |  [a-zA-Z0-9_-]+\\.[a-zA-Z0-9_]+
CVE | CVE-YYYY-XXXX |  CVE-\d{4}-\d{4,}

Figure 2: Data Augmentation Steps

We leverage the MLM (Masked Language Model) capability of the natural language
model to expand the dataset and address the limited samples problem of
TTPHunter for the remainder of the TTP class. For MLM, we employ the domain-
specific language model called SecureBERT [3]. In this process, we mask words
in each sentence with a special token $<mask>$ and employ SecureBERT to
predict the masked word using its MLM capability. SecureBERT provides a list
of candidate words and their corresponding probabilities, which maintain the
contextual meaning when replacing the masked word.

We can see at step \normalsize1⃝ in Fig. 2, an example of input sentence as
"Adversary obtained credentials using compromised systems". In this case, if
we mask the word "Adversary", then the model predicts possible words that
preserve the contextual meaning (step \normalsize2⃝ in Fig. 2). The
probabilities associated with each word indicate the confidence level of the
predicted word. We select the top $5$ words from this list and generate five
new sentences for each input sentence (step \normalsize3⃝ in Fig. 2). The
sentence’s meaning may deviate after replacing the masked word with the
predicted word. Therefore, we employ cosine similarity to compare each newly
generated sentence with the original sentence (step \normalsize4⃝ in Fig. 2)
and select the sentence with the highest similarity index. To compute the
cosine similarity, we generate contextual embedding for both the original and
generated sentences using Sentence Transformer [13]. The similarity score
ranges between $0$ (not similar) to $1$ (Exactly similar), and we set a
threshold $(\theta)$ of $0.975$. We retain only those sentences having
similarity scores greater than $\theta$. The sentence augmentation algorithm
is outlined in Algorithm 1, which we employ to construct the augmented
sentence-TTP dataset. More detailed information regarding the distribution of
the augmented sentence-TTP dataset is present in the section V-A.

###  IV-B Prepossessing & Fine-Tuning

The sentences present in the dataset consist of irrelevant structures, which
we fix during the pre-processing method and let the data add more value to the
dataset. First, we remove the citation references from these sentences, which
refer to past attack campaigns or threat reports. Further, we find various
IOCs (Indicator of Compromise) patterns present in the sentences, which
potentially obscure the contextual understanding of the sentences. For
example, IP and domain addresses, file paths, CVE IDs, emails, and registry
paths. We implement an IOC replacement method to overcome the obstruction
these patterns impose in sentences. This method uses regular expressions
(regex) to substitute IOC patterns with their respective base names. For
example, a sentence like "Upon execution, the malware contacts the C2 server
at attacker-example.com, drops an executable payload.exe at
C:$\backslash$Users$\backslash$Default$\backslash$AppData$\backslash$Roaming,
and creates an autorun entry in
HKEY_LOCAL_MACHINE$\backslash$Software$\backslash$Microsoft$\backslash$Windows$\backslash$CurrentVersion$\backslash$Run"
get transformed to "Upon execution, the malware contacts the C2 server at
domain, drops an executable file at file path, and creates an autorun entry in
registry". This method lets the model add more contextual information rather
than hindering the meaning, which helps better TTP identification. Table IV-A
details the considered IOCs example, their corresponding base name, and the
use of regex pattern. The processed sentences get passed further for fine-
tuning.

Figure 3: Fine tuning-steps

The finetuning process is similar to the TTPHunter’s finetuning. As TTPHunter
extracts sentence embedding from the traditional BERT model and passes it to a
linear classifier for classification, we employ a similar method in
TTPXHunter. It first extracts domain-specific embedding using the SecureBERT
language model and passes embedding to a linear classifier for TTP
classification. The finetuning process is meticulously orchestrated to
optimize performance on the processed sentence dataset. We initiate the
process by configuring essential parameters, setting the learning rate to
$1e-5$ to ensure subtle adjustments to the model, choosing a batch size of
$64$ to balance computational efficiency with training effectiveness, and
training it for $10$ epochs. We leverage the Hugging Face’s Transformers
library [9] for its robust support of transformer models. Sentences are
tokenized using SecureBERT’s tokenizer, aligning with its pre-trained
understanding of language structure, and inputs are standardized to a maximum
length of $256$ tokens. We finetune our model to let it understand the context
for ATT&CK TTP, which further enhances the classification capability. The
model’s finetuning is shown in Fig. 3.

###  IV-C TTP Extraction

TTPXHunter takes finished threat reports as input and breaks the report
contents into a list of individual sentences. Then, each sentence is processed
and passed to the TTPXHunter’s finetuning architecture for classification. The
system classifies each sentence to identify TTPs. Finally, it aggregates these
TTPs and creates a list of TTPs extracted from the analyzed report. A threat
report usually contains many irrelevant sentences that do not reflect TTPs.
However, our classification module is a closed-world solution (the input will
surely be classified into at least one target class). As a result, irrelevant
sentences can also be classified as one of the TTPs in the target class, which
can lead to huge false positives. To reduce this effect, we filter irrelevant
sentences, similar to TTPHunter. We employ a threshold mechanism in the
classification module to filter irrelevant sentences and only map sentences
that explain TTPs, i.e., a relevant sentence. We filter irrelevant sentences
based on classification confidence score. We fix a threshold $(\Theta)$ and
filter the sentences if the classifier’s confidence score is below the
threshold. We follow the same threshold value experimentally obtained in
TTPHunter, i.e., $0.644$.

Once the linear classifier extracts the list of TTPs present in the threat
report, TTPXHunter converts the list to the Structured Threat Information
eXpression (STIX) [18] format, significantly enhances cyber threat
intelligence operations. It supports detailed analysis and correlation of
threats by providing a rich, structured representation of cyber threat
information. This structured format facilitates automated processing and
threat response, which increases operational efficiency. Moreover, the
consistency and standardization offered by STIX improve communication within
and between organizations to ensure a common understanding of cyber threats.

##  V Experiments and Results

This section presents details about the prepared dataset and the experiments.
We also discuss the results obtained and chosen performance measures.

###  V-A Dataset

We compute model performance on our test dataset through sentence-to-TTP
mapping. However, in the real world, the threat data is in the form of reports
containing a set of sentences mixed with relevant and irrelevant sentences.
Therefore, we also evaluate the model’s performance report-wise. As a result,
we prepared two datasets to measure the efficiency of TTPXHunter and the
current literature: $1)$ The augmented Sentence-TTP dataset and $2)$ The
Report-TTP dataset.

####  V-A1 Augmented Sentence-TTP Dataset

To prepare the sentence-TTP dataset, we consider the TTPHunter dataset as a
base dataset, prepared using MITRE ATT&CK knowledgebase [2]. The base dataset
consists of two columns: sentences and their corresponding TTP ID. The dataset
consists of $10,906$ sentences over $193$ TTPs. We use our proposed data
augmentation algorithm, explained in Algorithm 1, and extend the dataset to
$39,296$ sentences distributed over $193$ TTP classes. The TTP ID $T1059$
(Command and Scripting Interpreter) consists of the highest number of
sentences as $800$, and TTP ID $T1127$ (Trusted Developer Utilities Proxy
Execution) consists of the lowest number of samples as $3$. On average, the
number of samples in our dataset is $203$. The distribution of data samples is
present in Appendix -A and a glimpse of the dataset is shown at step
\normalsize5⃝ in Fig 2.

####  V-A2 Report-TTP Dataset

Generally, threat data is present in the form of threat analysis reports.
Therefore, We evaluate TTPXHunter on a document dataset, which demonstrates
the performance of TTPXHunter in filtering irrelevant sentences from threat
reports. It also tells us how efficiently TTPXHunter can extract threat
intelligence from threat reports. We manually collect $149$ threat reports
published by various prominent security firms, and we manually label the set
of TTPs present in each report to prepare the ground truth. The document-TTP
dataset contains two columns: threat report and list of TTP present in the
corresponding threat report.

###  V-B Evaluation

We evaluate TTPXHunter using various performance metrics and compare its
performance with several current studies. As our dataset is imbalanced, shown
in Appendix Fig. 9, we consider macro-averaged precision, recall, and f1-score
[11]. This approach ensures balanced evaluation across all classes [29]. By
giving equal importance to each TTP class, these metrics prevent the majority
class’s dominance from overshadowing the minority class’s performance. It
promotes the development of effective and fair models across different TTP
classes and is essential for nuanced TTP classification tasks.

####  V-B1 Augmented Sentence-based Evaluation

We finetune TTPXHunter on the prepared augmented dataset and compare the other
two BERT-based models, i.e., TRAM [8] and TTPHunter [2] present in the
literature. We divide the prepared augmented dataset into train and test sets
with an $80:20$ ratio.

TTPXHunter vs TRAM :  We fine-tune the TTPXHunter on the train set and
evaluate its performance using the chosen performance metrics. Further, we
finetune the literature TRAM [8] on the same dataset and evaluate its
performance. By employing TRAM on the augmented dataset, we extend the
capability of TRAM from the 50 most frequently used TTPs to the full spectrum
of TTPs. As a result, it gives common ground for comparing TTPXHunter and
TRAM. The result obtained by both methods and their comparison is shown in
Fig. 4. As we can see, the TTPXHunter outperforms the TRAM, which reflects the
difference between contextual embedding of general scientific BERT and domain-
specific BERT embeddings. This result reflects that the domain-specific
language model provides a better contextual understanding of embedding than
the language model trained on general scientific terms.

Figure 4: Performance Comparison between TRAM [8] and TTPXHunter over
Augmented Dataset

TTPXHunter vs TTPHunter :  We assess the performance of our proposed
TTPXHunter alongside state-of-the-art TTPHunter. Our proposed extraction
method, TTPXHunter, performs better than state-of-the-art TTPHunter.
TTPXHunter’s superiority is due to using a cyber-domain-specific finetuned
language model. Sentences containing domain-specific terms, such as ”window”
and ”registry,” introduce a distinct context that differs from general
English. This distinction allows our method, based on the domain-specific
language model, to capture and interpret the contextual meaning more
accurately than traditional models. In addition, TTPXHunter can identify the
range of $193$ TTPs with $0.92$ f1-score, whereas TTPHunter is limited to only
$50$ TTPs. The improvement in the result and the capability to identify all
ranges of TTPs make TTPXHunter superior to TTPHunter.

Figure 5: Performance Comparison between TTPHunter [2] and TTPXHunter over
TTPHunter’s 50-TTP set

Further, to understand the efficiency of the data augmentation method and
compare the performance of TTPXHunter and TTPHunter on the same base, we
evaluate TTPXHunter on the ground of TTPHunter. We only selected 50 TTP sets
for which we developed TTPHunter and evaluated both. The obtained result is
shown in Fig. 5. As we can see, TTPXHunter outperforms TTPHunter on the 50-TTP
set ground of TTPHunter. It reflects that augmenting more samples for a 50-TTP
set and employing a domain-specific language model enables the classifier to
better understand the context of TTP.

####  V-B2 Report-based Evaluation

TABLE IV: Comparison with State-of-the-art methods over Report Dataset Model | Precision (%) | Recall (%) | F1-score (%) | Hamming Loss
---|---|---|---|---
ATTACKG [6] | $88.58$ | $95.22$ | $88.52$ | $0.14$
rcATT [10] | $30.47$ | $44.03$ | $30.56$ | $0.64$
Ladder [4] | $92.97$ | $95.73$ | $93.90$ | $0.10$
TRAM [8] | $94.54$ | $94.33$ | $93.49$ | $0.10$
TTPXHunter (Proposed) | 97.38 | 96.15 | 97.09 | 0.05

In the real world, we have threat reports in the form of natural language
rather than sentence-wise datasets, and these reports contain information
along with TTP-related sentences. So, we evaluate the TTPXHunter on the report
dataset, which contains each sample as threat report sentences and a list of
TTP explained in the report. Extracting TTPs from threat reports is a multi-
label problem because a list of TTP classes is expected as output for any
given sample, i.e., threat report in this case. The evaluation of such
classification also requires careful consideration because of multi-label
classification.

Evaluation Metrics: In the multi-label problem, the prediction vector appears
as a multi-hot vector rather than a one-hot vector in a multi-class problem.
In the multi-label case, there may be a situation where not all expected TTP
classes were predicted; instead, a subset of them is correctly predicted.
However, the prediction may be wrong because the whole multi-hot vector does
not match. For example, If the true label set contains $\\{T1,T2,T3\\}$ and
the predicted label is $\\{T2,T3\\}$, then it may be considered to be a
mismatch even though $T2$ and $T3$ are correctly classified. So, relying on
accuracy may not be a good choice for multi-label problems [28]; instead, we
consider hamming loss as a performance metric to deal with such a scenario.
The hamming loss measures the error rate label-wise [19, 21, 28]. It
calculates the ratio of incorrect labels to all labels. For given $k$ threat
reports, the hamming loss is defined as:

$\text{HL}=\frac{\sum_{i=1}^{k}[y_{i}\oplus\hat{y}_{i}]}{k}$ (1)

Where, $y_{i}\text{ and }\hat{y}_{i}$ are multi-hot predicted labels and true
label for $i^{th}$ instance, respectively. The $\oplus$ represents element-
wise exclusive OR (XOR) operation. The low hamming loss represents that models
make minimal wrong predictions.

Further, we also evaluate macro precision, recall, and f1-score by leveraging
a multi-label confusion matrix package from sklearn [11]. Then, we calculate
true positive, false positive, and false negative for each class and calculate
these performance metrics. Further, we calculate the macro average between all
classes to get macro-averaged performance metrics for all chosen measures,
i.e., precision, recall, and f1-score. We prefer the macro-average method to
ignore biases towards the majority class and provide equal weight to all
classes. We consider four state-of-the-art methods, i.e., [10, 6, 4, 8] for
comparison against TTPXHunter based on these metrics over the report dataset.
This comparison aims to understand the effectiveness of TTPXHunter over state-
of-the-art for TTP extraction from finished threat reports. These methods
provide the list of TTPs extracted from the given threat report and the model
confidence score for each. Out of all extracted TTPs, only relevant TTPs are
selected based on the threshold mechanism decided by each method. We evaluate
the state-of-the-art method’s performance based on the threshold value given
in their respective papers. For TTPXHunter, we obtain the same threshold
experimentally chosen for TTPHunter, i.e., $0.644$. The results obtained from
all implemented methods on our report dataset are shown in Table IV. It
demonstrates that TTPXHunter outperforms all implemented methods across all
chosen metrics, i.e., the lowest hamming loss and the highest other
performance metrics. It achieves the highest f1-score of $97.07\%$, whereas
out of all state-of-the-art methods, LADDER [4] performs better than other
state-of-the-art methods and achieves $2^{nd}$ highest performance of
$93.09\%$ F1-score. This performance gain over state-of-the-art methods
demonstrates the efficiency of the TTPXHunter, and we plan to make it open for
the benefit of the community.

As this experiment involves $193$ target TTP classes, it is challenging to
visualize the class-wise performance of the employed models. Therefore, we
follow a different way to assess the class-wise efficiency of the employed
models. We count the number of TTP classes whose chosen performance metrics
lie within a range. We employ a range interval of $0.1$, i.e., $10\%$, to
calculate the number of TTP classes whose score falls into the range.

We perform this calculation across all five methods and three chosen
performance metrics. The obtained results are present in Figures 6, 7, and 8.
The observation reveals that most TTP classes analyzed by rcATT fall within
the $0-0.10$ range, contributing to its overall lower performance. This
performance is due to the reliance on the TF-IDF method to transform sentences
into vectors. TF-IDF is a numerical statistic that reflects how important a
word is to a document in a collection or corpus, balancing its frequent
appearance within a document against its commonness across all documents [26,
20, 12]. This method lacks the ability to understand the context and semantic
relationships between words, making it unable to grasp the overall meaning of
sentences [16, 33]. ATTACKG, conversely, exhibits a lower score within the
$0-0.10$ range for certain TTP classes, which adversely affects its overall
performance. However, TRAM shows a minimum performance range of $0.3-0.4$ for
TTP classes, which indicates better performance than rcATT and ATTACKG. LADDER
ensures a performance score of at least $0.4-0.5$ for a TTP class, which
positions it ahead of the aforementioned methods, including rcATT, ATTACKG,
and TRAM. Our proposed model, TTPXHunter, assures a minimum score of $0.6-0.7$
for TTP classes, with the majority exhibiting scores between $0.9-1.0$, which
underscores TTPXHunter’s significant advantage over the other methods. It
demonstrates the effectiveness of domain-specific models for domain-specific
downstream tasks.

Figure 6: Class-wise Precision Score Comparison with State-of-the-art Methods
Figure 7: Class-wise Recall Score Comparison with State-of-the-art Methods
Figure 8: Class-wise F1 Score Comparison with State-of-the-art Methods

##  VI Limitations & Future Directions

In addition to the advantages of TTPXHunter, like threat intelligence
extraction, threat profiling, and sharing, it has some limitations that one
should be careful about while using for actionable insights. The MITRE ATT&CK
framework is not a kind of fixed knowledge base. Instead, MITRE threat
researchers are continuously updating it. One may need to finetune the model
again if new TTPs are added to get the newer TTPs predicted. While finetuning
on newer TTPs may require using our proposed data augmentation method to
create new augmented sentences specific to newer TTPs. Therefore, we plan to
make it public so one can adapt our method for any new upcoming versions of
the ATT&CK framework.

Further, the TTPXHunter contains a one-to-one classifier model, which maps a
given sentence to a single TTP. Like a single sentence, a sentence containing
one-to-many mapping may explain more than one TTP. For example, the sentence
is "The attacker gained initial access through a phishing email and obtained
persistence via run registry modification". TTPXHunter maps this sentence to
T1566 (Phishing) or T1037 (Boot or Logon Initialization Scripts) in such a
scenario. Extending the capability of TTPXHunter to identify such one-to-many
mapping can help us improve the model’s performance. We plan to take up this
challenge to improve the efficiency of TTPXHunter in the future.

##  VII Conclusion

This research demonstrates the efficiency of domain-specific language models
in extracting threat intelligence in terms of TTPs, which can share the attack
patterns and accelerate the threat response and detection mechanisms. The tool
TTPXHunter extends the TTPHunter’s capability over multiple dimensions, such
as expanding to the full spectrum of TTP extraction and improving efficiency
by leveraging domain-specific language models. We evaluate the efficiency of
TTPXHunter over the prepared augmented sentence-TTP dataset and report-TTP
dataset. On the augmented dataset, TTPXHunter outperforms both BERT-variant
models, i.e., TRAM and TTPHunter. TTPXHunter also outperforms the state-of-
the-art TTP extraction methods by achieving the highest F1 score and lowest
hamming loss. TTPXHunter’s performance over the report dataset demonstrates
the model’s efficiency in capturing relevant sentences from threat reports and
correctly classifying them to the TTP class. The conversion of extracted TTPs
to STIX makes integrating threat intelligence into security operations easier.
TTPXHunter aids in improving the threat analyst’s capability to share
intelligence, analyze threats, understand the modus operandi of sophisticated
threat actors, and emulate their behavior for red teaming. Therefore,
TTPXHunter can support various cybersecurity teams, including red, blue, and
purple teams in an organization.

## References

  * [1] Xander Bouwman, Harm Griffioen, Jelle Egbers, Christian Doerr, Bram Klievink, and Michel Van Eeten.  A different cup of $\\{TI\\}$? the added value of commercial threat intelligence.  In 29th USENIX security symposium (USENIX security 20), pages 433–450, 2020.
  * [2] Nanda Rani, Bikash Saha, Vikas Maurya, and Sandeep Kumar Shukla. ”TTPHunter: Automated Extraction of Actionable Intelligence as TTPs from Narrative Threat Reports.” In Proceedings of the 2023 Australasian Computer Science Week, pp. 126–134, 2023.
  * [3] Ehsan Aghaei, Xi Niu, Waseem Shadid, and Ehab Al-Shaer. ”SecureBERT: A Domain-Specific Language Model for Cybersecurity.” In International Conference on Security and Privacy in Communication Systems, pp. 39–56. Springer, 2022.
  * [4] Md Tanvirul Alam, Dipkamal Bhusal, Youngja Park, and Nidhi Rastogi. ”Looking beyond IoCs: Automatically extracting attack patterns from external CTI.” In Proceedings of the 26th International Symposium on Research in Attacks, Intrusions and Defenses, pp. 92–108, 2023.
  * [5] Ghaith Husari, Ehab Al-Shaer, Mohiuddin Ahmed, Bill Chu, and Xi Niu. ”Ttpdrill: Automatic and accurate extraction of threat actions from unstructured text of cti sources.” In Proceedings of the 33rd annual computer security applications conference, pp. 103–115, 2017.
  * [6] Zhenyuan Li, Jun Zeng, Yan Chen, and Zhenkai Liang. ”AttacKG: Constructing technique knowledge graph from cyber threat intelligence reports.” In European Symposium on Research in Computer Security, pp. 589–609. Springer, 2022.
  * [7] MITRE. ”ATT&CK Framework.” 2023. Available online: https://attack.mitre.org. [Accessed July 22, 2023].
  * [8] MITRE. ”Threat Report ATT&CK Mapper (TRAM).” 2023. Available online: https://github.com/center-for-threat-informed-defense/tram/. [Accessed Feb 22, 2024].
  * [9] Hugging Face. Transformers, 2024. Available online: https://huggingface.co/docs/transformers/en/index
  * [10] Valentine Legoy, Marco Caselli, Christin Seifert, and Andreas Peter. ”Automated retrieval of att&ck tactics and techniques for cyber threat reports.” arXiv preprint arXiv:2004.14322, 2020.
  * [11] F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay, ”Scikit-learn: Machine Learning in {P}ython,” Journal of Machine Learning Research, vol. 12, pp. 2825–2830, 2011.
  * [12] G. Salton, A. Wong, and C.-S. Yang, “A vector space model for automatic indexing,” _Communications of the ACM_ , vol. 18, no. 11, pp. 613–620, 1975, ACM New York, NY, USA.
  * [13] Nils Reimers and Iryna Gurevych.  Sentence-bert: Sentence embeddings using siamese bert-networks.  _arXiv preprint arXiv:1908.10084_ , 2019.
  * [14] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Łukasz Kaiser, and Illia Polosukhin.  Attention is all you need.  _Advances in neural information processing systems_ , 30, 2017.
  * [15] Nafiz Rifat, Mostofa Ahsan, Md Chowdhury, and Rahul Gomes, “BERT against social engineering attack: Phishing text detection,” in 2022 IEEE International Conference on Electro Information Technology (eIT), IEEE, 2022, pp. 1–6.
  * [16] S. Selva Birunda and R. Kanniga Devi, ”A review on word embedding techniques for text classification,” in Innovative Data Communication Technologies and Application: Proceedings of ICIDCA 2020, pp. 267–281, Springer, 2021.
  * [17] M. Tikhomirov, N. Loukachevitch, A. Sirotina, and B. Dobrov, “Using BERT and augmentation in named entity recognition for cybersecurity domain,” in Natural Language Processing and Information Systems: 25th International Conference on Applications of Natural Language to Information Systems, NLDB 2020, Saarbrücken, Germany, June 24–26, 2020, Proceedings 25, Springer, 2020, pp. 16–24.
  * [18] S. Barnum, “Standardizing cyber threat intelligence information with the structured threat information expression (STIX),” Mitre Corporation, vol. 11, pp. 1–22, 2012.
  * [19] A. C. P. L. F. de Carvalho and A. A. Freitas, “A tutorial on multi-label classification techniques,” in Foundations of Computational Intelligence Volume 5: Function Approximation and Classification, Springer, 2009, pp. 177–195.
  * [20] K. Sparck Jones, “A statistical interpretation of term specificity and its application in retrieval,” _Journal of Documentation_ , vol. 28, no. 1, pp. 11–21, 1972, MCB UP Ltd.
  * [21] M.-L. Zhang and Z.-H. Zhou, “A review on multi-label learning algorithms,” IEEE Transactions on Knowledge and Data Engineering, vol. 26, no. 8, pp. 1819–1837, 2013, IEEE.
  * [22] Beltagy, Iz and Lo, Kyle and Cohan, Arman. “SciBERT: A pretrained language model for scientific text.” arXiv preprint arXiv:1903.10676, 2019.
  * [23] Daszczyszak, Roman and Ellis, Dan and Luke, Steve and Whitley, Sean.  TTP-Based Hunting.  MITRE CORP MCLEAN VA, Tech. Rep, 2019.
  * [24] B. Tang, J. Wang, Z. Yu, B. Chen, W. Ge, J. Yu, and T. Lu, ”Advanced Persistent Threat intelligent profiling technique: A survey,” Computers and Electrical Engineering, vol. 103, pp. 108261, 2022, Elsevier.
  * [25] Rahman, Md Rayhanur and Williams, Laurie. ”From Threat Reports to Continuous Threat Intelligence: A Comparison of Attack Technique Extraction Methods from Textual Artifacts.” arXiv preprint arXiv:2210.02601 (2022).
  * [26] G. Salton and M.E. Lesk, “Computer evaluation of indexing and text processing,” _Journal of the ACM (JACM)_ , vol. 15, no. 1, pp. 8–36, 1968, ACM New York, NY, USA.
  * [27] Md Rayhanur Rahman, Rezvan Mahdavi Hezaveh, and Laurie Williams.  What are the attackers doing now? Automating cyberthreat intelligence extraction from text on pace with the changing threat landscape: A survey.  ACM Computing Surveys, 55(12):1–36, 2023, ACM New York, NY.
  * [28] Bikash Saha, Nanda Rani, and Sandeep Kumar Shukla.  MalXCap: A Method for Malware Capability Extraction.  In International Conference on Information Security Practice and Experience, pages 230–249. Springer, 2023.
  * [29] Grandini, Margherita and Bagli, Enrico and Visani, Giorgio.  Metrics for multi-class classification: an overview.  _arXiv preprint arXiv:2008.05756_ , 2020.
  * [30] Bader Al-Sada, Alireza Sadighian, and Gabriele Oligeri. “MITRE ATT&CK: State of the Art and Way Forward,” arXiv preprint arXiv:2308.14016, 2023.
  * [31] Yinghai Zhou, Yi Tang, Ming Yi, Chuanyu Xi, and Hai Lu.  CTI view: APT threat intelligence analysis system.  _Security and Communication Networks_ , 2022:1–15, 2022.  Hindawi Limited.
  * [32] Abdul Basit Ajmal, Munam Ali Shah, Carsten Maple, Muhammad Nabeel Asghar, and Saif Ul Islam.  Offensive security: Towards proactive threat hunting via adversary emulation.  IEEE Access, 9:126023–126033, 2021.
  * [33] R. Patil, S. Boit, V. Gudivada, and J. Nandigam, ”A survey of text representation and embedding techniques in nlp,” IEEE Access, 2023, IEEE.
  * [34] O.C. Briliyant, N.P. Tirsa, and M.A. Hasditama, “Towards an automated dissemination process of cyber threat intelligence data using STIX,” in _2021 6th International Workshop on Big Data and Information Security (IWBIS)_ , pp. 109–114, 2021, IEEE.

###  -A Sentence-TTP Dataset Distribution

This section plots the Sentence-TTP dataset distributed over the $193$-TTP
classes. The sentence-TTP dataset contains sentences as data sample and their
corresponding TTP ID. The number of samples in each TTP class is shown in Fig
9. In this figure, each tile represents a block for each TTP class, and
contains TTP ID and their corresponding number of samples present in the
dataset.

Figure 9: Sentence-TTP Dataset Data Distribution over 193-TTP Class


# An Axiomatic Approach to Detect Information Leaks in Concurrent Programs

Sandip Ghosal  Department of Computer Science & Engineering
Indian Institute of Technology, Bombay
Mumbai, India
<EMAIL_ADDRESS>R. K. Shyamasundar  Department of Computer Science &
Engineering
Indian Institute of Technology, Bombay
Mumbai, India
<EMAIL_ADDRESS>
###### Abstract

Realizing flow security in a concurrent environment is extremely challenging,
primarily due to non-deterministic nature of execution. The difficulty is
further exacerbated from a security angle if sequential threads disclose
control locations through publicly observable statements like print, sleep,
delay, etc. Such observations lead to internal and external timing attacks.
Inspired by previous works that use classical Hoare style proof systems for
establishing correctness of distributed (real-time) programs, in this paper,
we describe a method for finding information leaks in concurrent programs
through the introduction of leaky assertions at observable program points.
Specifying leaky assertions akin to classic assertions, we demonstrate how
information leaks can be detected in a concurrent context. To our knowledge,
this is the first such work that enables integration of different notions of
non-interference used in functional and security context. While the approach
is sound and relatively complete in the classic sense, it enables the use of
algorithmic techniques that enable programmers to come up with leaky
assertions that enable checking for information leaks in sensitive
applications.

##  I Introduction

Information flow control (IFC) in sequential and concurrent programs has been
an active area of research for over two decades. While researchers have
developed specification approaches [1, 2, 3, 4] and enforcement mechanisms for
sequential programs [5, 6, 7, 8, 9, 10, 11], flow security in concurrent
programs remains a challenge primarily due to covert channels that could leak
secret information. Timing channels in concurrent programs are the most
commonly known covert channels.

⬇

1await sem>0 then

2 sem = sem - 1;

3 print(‘a’);

4 v = v+1;

5 print(‘b’);

6 sem = sem + 1;

⬇

1print(‘c’);

2if h then

3 await sem>0 then

4 sem = sem - 1;

5 v = v+2;

6 sem = sem + 1;

7else

8 skip;

9print(‘d’);

Figure 1: (a) Process $T_{1}$ (left); (b) Process $T_{2}$ (right)

For instance, often programs encode secret information in such a way that
allow an attacker to learn about confidential data by observing time
variations between interleaving execution of assignments to public variables
or output statements such as print, or the availability of shared resources in
a particular time interval. Recent flow security enforcing mechanisms for
sequential programs [12, 6] identify information leaks in individual threads,
but the approaches are too restrictive for programs that reveal the control
position through the observable output statements. For example, consider the
program shown in Figure 1, (Cf. [13]) where $h$ is a secret variable, and
await command is a conditional critical region. The await command essentially
represents a number of standard synchronization primitives including
semaphores. Let us suppose that process $T_{1}$ holds the semaphore and
executes the critical region as an indivisible operation. Then, output ‘acdb’
arising due to concurrent executions of $T_{1}$ and $T_{2}$ reveal the value
of $h$ as 0. There have been a few efforts aiming to prevent timing leaks in
concurrent or multi-threaded programs [14, 15, 16, 17, 18, 19, 20, 21] but
majorly have sidestepped the issue that arise due to output statements.

In this paper, we aim to preserve the confidentiality of programs in a
concurrent context preventing an attacker external to the system from gaining
knowledge about secret information through observations of program outputs. We
describe an axiomatic approach that establishes functional correctness [22] in
a parallel context to realize the insecurity at a program point that might
leak information due to concurrent executions. In the envisaged work, we
introduce auxiliary time variables that capture execution time for each
execution step and enables us to derive a notion of leaky assertion for each
public program locations, that when satisfied, one can conclude that the
program leaks out information. Enforcing functional non-interference in a
concurrent setting that uses leaky assertions leads to the identification of
plausible information leaks at various program locations. Our proposed
approach is primarily motivated by approaches used by Lamport and Schneider
[23, 24, 25, 26] on the correctness of real-time distributed programs. Similar
to these approaches using time as an ordinary variable for specifying and
reasoning about real-time systems, we we arrive at leaky assertions using an
external time variable. With such a specification leaky and standard
assertions for concurrent programs, we check for non-interference using
verification conditions similar to those used in ‘Gries-Owicki’ [22]. By
showing the program is non-interference, we infer information leaks through
the leaky assertions embedded in the specification.

Main contributions of the paper are:

  1. 1

Introduction of leaky assertions when embedded in concurrent program
specifications, enables detection of information leaks once the proof of
components of the concurrent programs are shown to be correct when considered
in isolation and are further shown to be interference free.

  2. 2

Demonstration of the method of embedding leaky assertions in standard
concurrent program specification [22], can be used to assert information
leaks, from which the information leaks are detected.

  3. 3

Checking for information leaks due to public observers like IO and time
sensitive operations (those that could disclose program locations through
output statements or observable timing channels), in non-interferring flow
secure concurrent programs [27].

Rest of the paper is organized as follows. Section II provides an abstract
syntax of the concurrent language. Section III briefly describes the necessary
background on correctness of concurrent programs and non-interference. Section
IV illustrates our solution followed by a formal description of our approach
and proof of soundness in Section V. Section VI compares our approach with
other related work in the literature, followed by conclusions in Section VII.

##  II Language Syntax

Before proceeding with the solution, we shall briefly describe the syntax of
the language we use.

Let $s$ ranging over set $S$ be the set of commands, $x$ be the set of
variables ranging over $X$, and $e$ denote an expression. Language primarily
comprises basic actions such as skip, assignment, sequence and control
statements such as conditional branch, iteration, await as in [22]. In
addition, we consider two statements print(e) and delay($e$) that serve as
observable points from the perspective of security and hence, these statements
are often termed public statements. Statement print($e$) writes $\llbracket
e\rrbracket$, where $\llbracket.\rrbracket$ denotes the classic evaluation of
expressions, into the standard output file that is visible to public. On the
other hand, delay($e$) postpones the current execution for $\llbracket
e\rrbracket$ time units. The abstract syntax of the language is given below:

$s$ ::= |  skip $|$ $x=e$ $|$ $s_{1};s_{2}$ $|$ if $e$ then $s_{1}$ else $s_{2}$
---|---
|  $|$ while $e$ do $s$ done $|$ print($e$) $|$ delay($e$)
|  $|$ $s_{1}\parallel s_{2}$ $|$ await $b$ then $s$

Operator $s_{1}\parallel s_{2}$ denotes a parallel (or concurrent) composition
of sequential programs $s_{1}$ and $s_{2}$. The await command is a conditional
critical region, that turns a statement $s$ into an indivisible action, is
executed in a state that satisfies condition $b$. The semantics of sequential
part of our language essentially follows the classical while-language.
Whereas, the semantics for concurrent composition and await statements are in
line with the transition rules given in [28].

##  III Correctness of Concurrent Programs

The seminal work of Hoare [29] provided a basis for establishing axiomatic
correctness of imperative programs. Let $P$ and $Q$ be assertions referred to
as pre-condition and post-condition for program/statement $S$. Hoare’s triple
specification for partial correctness of program $S$, is denoted
$\\{P\\}S\\{Q\\}$ with the following interpretation: if pre-condition $P$ is
true before execution of $S$, then post-condition $Q$ holds if and when the
execution of $S$ terminates.

Owicki and Gries [22] generalized Hoare’s axiomatic approach for shared
variable concurrency with the introduction of non-interference (functional) of
programs. Let $S_{i}$ for i =1,…n, be sequential programs. $S_{1}\parallel
S_{2}\parallel\dots\parallel S_{n}$ denotes concurrent composition. The effect
of concurrent execution is the same as executing each $S_{i}$ as an
independent program if the programs are disjoint. If the programs are not
disjoint, then, it is necessary that programs be interference free. Non-
interference requires that assertions used in the proof
$\\{P_{i}\\}S_{i}\\{Q_{i}\\}$ for each process remain validated under
concurrent execution of the other processes. Let, $T$ be a statement in
program $S_{i}$. Then, concurrent execution of
$\\{P_{1}\\}S_{1}\\{Q_{1}\\},\dots,\\{P_{n}\\}S_{n}\\{Q_{n}\\}$ is said to be
non-interfering if $T$ does not interfere with $\\{P_{j}\\}S_{j}\\{Q_{j}\\}$
where $i\neq j$. Formal definition is given below.

######  Definition 1 (Correctness).

Given a proof $\\{P\\}S\\{Q\\}$ and a statement $T$ with the pre-condition
$pre(T)$, the statement $T$ is said to be non-interfering with
$\\{P\\}S\\{Q\\}$ if the following two conditions hold:

  1. 1

$\\{Q\wedge pre(T)\\}T\\{Q\\}$;

  2. 2

$\\{pre(S^{\prime})\wedge pre(T)\\}T\\{pre(S^{\prime})\\}$ where, $S^{\prime}$
is an await or assignment statement within $S$ but not within an await block.

##  IV Capturing Information Leaks Through Output

The crux of our approach lies in setting observers from which one can draw
inference about information leaks. Observation points allow us to deduce how
long a process could wait at a control point relative to another process at
some other control point wherein the two processes share information via
shared variables (could be sensitive) through synchronization. This is
realized through auxiliary variables that are used in the specification of
concurrent programs. Lamport [25] illustrates an effective use of auxiliary
variables for establishing correctness of real-time programs.

Timing constraints for the waiting time that impose upper or lower bound for
an action to occur can be expressed using auxiliary (time) variables. Semantic
characterization of time constraints required for mutual exclusion and
analysis of bounded waiting time is similar to that shown in [25].

###  IV-A Illustrative Example

Let us illustrate that the labelled program $T_{2}$ showin in Figure 2, where
labels denote identifiers for statements as well as locations of program
control does indeed leak information via public statements. Labels $l_{0}$ and
$l_{8}$ are the entry and exit labels respectively. Let us mark the execution
time of the program at specific program locations using auxiliary variable
$t$.

⬇

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{0}:$
$\mathbf{\langle\langle t=T\rangle\rangle}$ print(‘c’);

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{1}:$ if h
then

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{2}:$
await sem>0 then

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{3}:$ sem
= sem - 1;

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{4}:$ v =
v+2;

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{5}:$ sem
= sem + 1

else

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{6}:$
skip;

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{7}:$
$\mathbf{\langle\langle t=t^{\prime}\rangle\rangle}$ print(‘d’);

$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}l_{8}:$

Figure 2: Process $T2$ (Cf. Figure 1) with auxiliary variable $t$

Execution of statements $l_{3}$ to $l_{5}$ is subject to availability of
$sem$, and hence, involves a delay, say $\Delta t$. Now, an observer can
easily measure the intermediate time difference between execution of public
statements $l_{0}$ and $l_{7}$ and just a comparison with $\Delta t$ would
enable him to deduce that information in $h$ more deterministic (informally,
cardinality of the set of possible values gets reduced from the original set
of possibilities) than he could infer otherwise.

$\displaystyle\footnotesize\begin{array}[]{c}\dfrac{[at\\_l_{0}]:t=T\quad[at\\_l_{7}]:t=t^{\prime}\quad
t^{\prime}-T\ll\Delta t}{h=0}\\\ \\\
\dfrac{[at\\_l_{0}]:t=T\quad[at\\_l_{7}]:t=t^{\prime}\quad
t^{\prime}-T\geqslant\Delta t}{h=1}\\\ \end{array}$

In short, our approach is based on specifying postulates of leaky assertions
at expected control points in the program and establish correctness of the
program in a standard manner. Once the proof is established, the leaky
assertions locations indicate the points of leakage of information; the actual
path can be derived using the semantic rules of the language for the program.

Thus, embedding leaky assertions in the specification of functional
correctness (Definition 1) of programs leads to a proof system that enables
asserting leaks in the programs . Let $S$ to be an assignment or a non-nested
await statement from the thread $T_{1}$. Let $P$ and $Q$ be pre- and post-
conditions of $S$ respectively. Then, proof of $\\{P\\}S\\{Q\\}$ asserts that
the leaky assertions hold when $T_{1}$ and $T_{2}$ execute concurrently.

  1. 1

$\\{Q\hskip 8.53581pt\wedge\hskip
8.53581pt((([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\ll\Delta t)\implies(h=0))\hskip 8.53581pt\vee\hskip
8.53581pt(([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\geqslant\Delta t)\implies(h=1)))\\}$
print(‘d’)
$\\{Q\\}$

  2. 2

$\\{P\hskip 8.53581pt\wedge\hskip
8.53581pt((([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\ll\Delta t)\implies(h=0))\hskip 8.53581pt\vee\hskip
8.53581pt(([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\geqslant\Delta t)\implies(h=1)))\\}$
print(‘d’)
$\\{P\\}$

  3. 3

$\\{((([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\ll\Delta t)\implies(h=0))\hskip 8.53581pt\vee\hskip
8.53581pt(([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\geqslant\Delta t)\implies(h=1)))\hskip 8.53581pt\wedge\hskip
8.53581ptP\\}$
S
$\\{((([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\ll\Delta t)\implies(h=0))\hskip 8.53581pt\vee\hskip
8.53581pt(([at\\_l_{0}]:t=T\wedge[at\\_l_{7}]:t=t^{\prime}\wedge
t^{\prime}-T\geqslant\Delta t)\implies(h=1)))\\}$

Note that the leaky assertions successfully capture the execution time
inconsistencies for both the cases where semaphore $sem$ is locked or released
by the process $T_{1}$. Therefore, the assertions remain unaffected by the
pre-and post-conditions for any statement $S$ in $T_{1}$. As the assertions
always hold good, this invariably proves the program as leaky.

Remarks: It is interesting to understand the impact if the program contains a
delay statement; suppose the statement skip is replaced by delay(50) – a delay
of 50ms (milliseconds for instance). Now, consider the following cases with
respect to the leaky assertions:

  1. 1

$\Delta t\ll 50ms:$

$\displaystyle\dfrac{[at\\_l_{0}]:t=T\quad[at\\_l_{7}]:t=t^{\prime}\quad\Delta
t\ll(t^{\prime}-T)\geq 50ms}{h=0}$
$\displaystyle\dfrac{[at\\_l_{0}]:t=T\quad[at\\_l_{7}]:t=t^{\prime}\quad\Delta
t\leq(t^{\prime}-T)\ll 50ms}{h=1}$

  2. 2

$\Delta t\gg 50ms:$

$\displaystyle\dfrac{[at\\_l_{0}]:t=T\quad[at\\_l_{7}]:t=t^{\prime}\quad\Delta
t\gg(t^{\prime}-T)\geq 50ms}{h=0}$
$\displaystyle\dfrac{[at\\_l_{0}]:t=T\quad[at\\_l_{7}]:t=t^{\prime}\quad\Delta
t\leq(t^{\prime}-T)\gg 50ms}{h=1}$

  3. 3

$\Delta t\approx 50ms:$
It would be difficult to postulate leaky assertion as an observer cannot
easily determine the execution path for $h=0$ or $h=1$; hence, the program may
be considered secure even though it may not be; note that axiomatic proof is
relative to the specifications.

##  V Formalization of our Approach

In our two-language approach for establishing leaks, if we can show that
assertions at various program points imply information leaks, then we would
have established that the program is not-secure; in other words, it is leaky.
Thus, if we establish that the program is insecure, we would have established
a counter-example; on the other hand, if we establish that the program is
secure, it would imply that the program is secure relative to the given
specification. Below, we establish the first from which the second follows
naturally.

######  Definition 2 (Leaky Assertion).

For a given set of assertions $\langle a_{0},\dots,a_{n}\rangle$ at respective
control points $\langle\ell_{0},\dots,\ell_{n}\rangle$ of the given program
$S$, using a nonempty set of sensitive (or high) variables $h_{1},\dots,h_{m}$
of the program, is said to be leaky if $a_{i}$ determinizes the value of at
least one of its’ sensitive variables, say $h_{j}$.

As discussed earlier, we say that an execution is leaky if the proof of the
program does not invalidate any of the leaky assertions.

######  Definition 3 (Leaky Execution).

Given a proof of $\\{P\\}S\\{Q\\}$ (we ignore global invariant as given in
[22]), where $S$ is an assignment or non-nested await statement, and a program
$T$ with at least one output statement with leaky assertion $A$ as it’s pre-
condition, concurrent execution of $S$ and $T$ is said to be leaky if the
following two conditions hold:

  1. 1

$\\{Q\wedge A\\}T\\{Q\\}$

  2. 2

$\\{P\wedge A\\}T\\{P\\}$

######  Proposition 1.

Let $\\{P\\}S\\{Q\\}$ be given and let $T$ be a statement with pre-condition
$A$, where $P$, $Q$ and $A$ are security assertions. If [$S\parallel T$] is
leaky then there exists at least one leaky assertion that determinizes
information in at least one secret variable.

######  Theorem 1 (Soundness).

Given the proof of $\\{P\\}S\\{Q\\}$ that has a leaky assertion $A_{i}$ at
control point $\ell_{i}$ within program $S$, then there exists an execution
path that leads to truth of $A_{i}$.

###### Proof.

Follows straight from the proof of $\\{P\\}S\\{Q\\}$. ∎

Issues of completeness also follow on the same lines.

Application to Flow Security:
Dynamic labelling (DL) algorithms [30] are in use for compile-time flow
security certification. For a program performing IO, however, the DL algorithm
could also be effectively used for identifying program points for arriving at
leaky assertions at plausible control points. DL algorithm binds subjects and
objects of a program with the given static or dynamic labels from a security
lattice [31] and evaluates the program as per the flow policy that enforces
information flow only in upward direction of the lattice. For standard output,
a static label low is assigned denoting least confidential policy. The output
statements controlled by sensitive variables that are labelled with higher
security labels would cause an information flow from higher label to low,
violating flow policy; thus, the algorithm easily highlights public statements
with possible sensitivities. Now, one could visualize the interactions of the
various concurrent components that could possibly interfere in the functional
sense. Using such an intuition, one could come up with different leaky
assertions that would detect information leaks.

The process of finding information leak in programs that perform IO could be
automated through the following steps: (i) first use DL algorithm to identify
the public statements that could leak information; (ii) capture time-
sensitivity for deriving leaky assertions corresponding to those public
statements using various analysis tools or oracles; (iii) arrive at possible
interaction of components at these public locations, and (iv) apply model
checkers to check for certain properties in components assuming possible
assertions in other components. We are working on arriving such algorithmic
techniques for detecting information leaks.

##  VI Related Work

In this section, we briefly highlight some of the important approaches in the
literature to prevent timing leaks in concurrent settings. In particular, we
focus on the solution that prevents leaking information through publicly
observable control points.

Our idea is primarily motivated by the work shown in [22, 32, 33]. The first
one presented flow proof rules that use correctness properties given in [22].
The last two approaches have given a semantic interpretation of non-
interference using Hoare-like logic. However, the goal of the above approaches
is to establish flow security of programs, whereas we aim to find information
leaks due to IO statements and time-sensitive operations using simple
inference.

Le Guernic [13] first envisages the potential danger in the use of output
statements in concurrent programs, and initial solution that motivated us to
provide an alternative approach in the form or security assertions. In this
approach, the author develops a run-time monitor that works in tandem with a
security automaton to decide whether to allow, deny or modify executions of
output statements and synchronization commands, particularly those appear in a
branch conditioned on sensitive variables. The automaton forbids executions of
output statements in this situation. Further, it acquires locks of
synchronization command before evaluating such a conditional. For instance,
acquiring semaphore $sem$ in the program shown in Figure 1 would prevent from
outputting “acdb”. The approach provides a thoughtful solution; nonetheless,
it is too restrictive. E.g., in the absence of an output statement, say
print(‘c’), the program is harmless, but as per the above solution executing
the program would still be dangerous. The axiomatic approach proposed in this
paper removes such restrictions on the program. Our approach enables us to
assert flow insecurity in the program methodically through the “Gries-Owicki”
conditions for functional correctness, thus overcomes the cases of false
alarms.

Other than the above approach, the majority of the mechanisms found in the
literature to prevent timing leaks in concurrent programs are based on either
(i) developing a sound typing rules to enforce secure-flow properties in
concurrent programming languages [19, 21]; (ii) performing source
transformation to balance the time variation or eliminate the timing channel
[18, 20, 34]; or (iii) developing a run-time monitor to identify potentially
dangerous executions that could leak information [14, 35, 36].

##  VII Conclusions and Future Work

In this paper, we have proposed an axiomatic proof system using leaky
assertions placed at output statement locations. To the best of our knowledge,
we are the first to propose an axiomatic approach using approaches for
establishing correctness of real-time distributed programs to analyze
information leaks in concurrent programs that have observable public
locations, leading to the following advantages: (i) it enables to formally
prove the presence of information leaks; (ii) aids in integrating the notions
of non-interference used in functional and security contexts with respect to
complete information flow models like that of Dorothy Denning [31], for shared
variable programs.

We are working towards automating the process of detecting information leaks
in concurrent programs that exhibit execution progress through public
statements. Automation has potential use in flow security certification of
concurrent programs to identify information leaks via sensitive public
statements. Initial work shows that DL algorithm can be integrated with model
checkers for validating/speculating leaky assertions.

## References

  * [1] S. Zdancewic and A. C. Myers, “Observational determinism for concurrent program security,” in _16th IEEE Computer Security Foundations Workshop, 2003. Proceedings._ IEEE, 2003, pp. 29–43.
  * [2] G. Boudol and I. Castellani, “Noninterference for concurrent programs and thread systems,” _Theoretical Computer Science_ , vol. 281, no. 1-2, pp. 109–130, 2002.
  * [3] D. M. Volpano, C. E. Irvine, and G. Smith, “A sound type system for secure flow analysis,” _Journal of Computer Security_ , vol. 4, no. 2/3, pp. 167–188, 1996.
  * [4] J. A. Goguen and J. Meseguer, “Security policies and security models,” in _IEEE Symposium on SP_ , 1982, pp. 11–11.
  * [5] P. Buiras, D. Vytiniotis, and A. Russo, “HLIO: Mixing static and dynamic typing for information-flow control in haskell,” in _ACM SIGPLAN Notices_ , vol. 50, no. 9. ACM, 2015, pp. 289–301.
  * [6] D. Stefan, A. Russo, J. C. Mitchell, and D. Mazières, “Flexible dynamic information flow control in haskell,” in _ACM Sigplan Notices_ , vol. 46, no. 12, 2011, pp. 95–106.
  * [7] L. Zheng and A. C. Myers, “Dynamic security labels and static information flow control,” _International Journal of Information Security_ , vol. 6, no. 2-3, pp. 67–84, 2007.
  * [8] C. Hammer and G. Snelting, “Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs,” _Int. Journal of Information Security_ , vol. 8, no. 6, pp. 399–422, 2009.
  * [9] V. Simonet and I. Rocquencourt, “Flow caml in a nutshell,” in _Proc. of 1st APPSEM-II workshop_ , 2003, pp. 152–165.
  * [10] A. C. Myers, L. Zheng, S. Zdancewic, S. Chong, and N. Nystrom, “Jif: Java information flow,” _http://www.cs.cornell.edu/jif_ , 2001.
  * [11] D. E. Denning and P. J. Denning, “Certification of programs for secure information flow,” _Communications of the ACM_ , vol. 20, no. 7, pp. 504–513, 1977.
  * [12] P. Buiras, D. Stefan, and A. Russo, “On dynamic flow-sensitive floating-label systems,” in _Proc. of IEEE 27th CSF Symposium_ , 2014, pp. 65–79.
  * [13] G. Le Guernic, “Automaton-based confidentiality monitoring of concurrent programs,” in _20th IEEE Computer Security Foundations Symposium (CSF’07)_. IEEE, 2007, pp. 218–232.
  * [14] M. Vassena, G. Soeller, P. Amidon, M. Chan, J. Renner, and D. Stefan, “Foundations for parallel information flow control runtime systems,” in _International Conference on Principles of Security and Trust_. Springer, 2019, pp. 1–28.
  * [15] M. Vassena, J. Breitner, and A. Russo, “Securing concurrent lazy programs against information leakage,” in _2017 IEEE 30th Computer Security Foundations Symposium (CSF)_. IEEE, 2017, pp. 37–52.
  * [16] A. Popescu, J. Hölzl, and T. Nipkow, “Formal verification of language-based concurrent noninterference,” _Journal of Formalized Reasoning_ , vol. 6, no. 1, pp. 1–30, 2013.
  * [17] G. Barthe, T. Rezk, A. Russo, and A. Sabelfeld, “Security of multithreaded programs by compilation,” _ACM Transactions on Information and System Security (TISSEC)_ , vol. 13, no. 3, pp. 1–32, 2010.
  * [18] A. Russo, J. Hughes, D. Naumann, and A. Sabelfeld, “Closing internal timing channels by transformation,” in _Annual Asian Computing Science Conference_. Springer, 2006, pp. 120–135.
  * [19] G. Smith _et al._ , “A new type system for secure information flow.” in _CSFW_ , vol. 1, 2001, p. 4.
  * [20] J. Agat, “Transforming out timing leaks,” in _Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages_ , 2000, pp. 40–53.
  * [21] G. Smith and D. Volpano, “Secure information flow in a multi-threaded imperative language,” in _Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages_. ACM, 1998, pp. 355–364.
  * [22] S. Owicki and D. Gries, “An axiomatic proof technique for parallel programs i,” _Acta informatica_ , vol. 6, no. 4, pp. 319–340, 1976.
  * [23] F. B. Schneider, B. Bloom, and K. Marzullo, “Putting time into proof outlines,” in _Workshop/School/Symposium of the REX Project (Research and Education in Concurrent Systems)_. Springer, 1991, pp. 618–639.
  * [24] L. Lamport, “An assertional correctness proof of a distributed algorithm,” _Science of Computer Programming_ , vol. 2, no. 3, pp. 175–206, 1982.
  * [25] ——, “Real time is really simple,” _Microsoft Research_ , pp. 2005–30, 2005.
  * [26] M. Abadi and L. Lamport, “An old-fashioned recipe for real time,” _ACM Transactions on Programming Languages and Systems (TOPLAS)_ , vol. 16, no. 5, pp. 1543–1571, 1994.
  * [27] G. R. Andrews and R. P. Reitman, “An axiomatic approach to information flow in programs,” _ACM Transactions on Programming Languages and Systems (TOPLAS)_ , vol. 2, no. 1, pp. 56–76, 1980.
  * [28] S. Brookes, “Full abstraction for a shared-variable parallel language,” _Information and Computation_ , vol. 127, no. 2, pp. 145–163, 1996.
  * [29] C. A. R. Hoare, “An axiomatic basis for computer programming,” _Communications of the ACM_ , vol. 12, no. 10, pp. 576–580, 1969.
  * [30] S. Ghosal, R. K. Shyamasundar, and N. V. N. Kumar, “Static security certification of programs via dynamic labelling,” in _Proceedings of the 15th International Joint Conference on e-Business and Telecommunications, ICETE 2018 - Volume 2: SECRYPT, Porto, Portugal, July 26-28, 2018._ , 2018, pp. 400–411.
  * [31] D. E. Denning, “A lattice model of secure information flow,” _CACM_ , vol. 19, no. 5, pp. 236–243, 1976.
  * [32] T. Amtoft and A. Banerjee, “Information flow analysis in logical form,” in _International Static Analysis Symposium_. Springer, 2004, pp. 100–115.
  * [33] L. Beringer and M. Hofmann, “Secure information flow and program logics,” in _20th IEEE Computer Security Foundations Symposium (CSF’07)_. IEEE, 2007, pp. 233–248.
  * [34] A. Russo and A. Sabelfeld, “Security for multithreaded programs under cooperative scheduling,” in _International Andrei Ershov Memorial Conference on Perspectives of System Informatics_. Springer, 2006, pp. 474–480.
  * [35] D. Stefan, A. Russo, P. Buiras, A. Levy, J. C. Mitchell, and D. Maziéres, “Addressing covert termination and timing channels in concurrent information flow systems,” in _ACM SIGPLAN Notices_ , vol. 47, no. 9, 2012, pp. 201–214.
  * [36] A. Askarov, S. Chong, and H. Mantel, “Hybrid monitors for concurrent noninterference,” in _2015 IEEE 28th Computer Security Foundations Symposium_. IEEE, 2015, pp. 137–151.