Threat Repair with Optimization Modulo Theories Thorsten Tarrach1 Masoud Ebrahimi2 Sandra König1 Christoph

2025-05-06 0 0 9.75MB 27 页 10玖币

侵权投诉

Threat Repair with Optimization Modulo

Theories

Thorsten Tarrach1, Masoud Ebrahimi2, Sandra König1, Christoph

Schmittner1, Roderick Bloem2, and Dejan Nickovic1

1AIT Austrian Institute of Technology

2Graz University of Technology

Abstract. We propose a model-based procedure for automatically pre-

venting security threats using formal models. We encode system models

and potential threats as satisﬁability modulo theory (SMT) formulas.

This model allows us to ask security questions as satisﬁability queries. We

formulate threat prevention as an optimization problem over the same

formulas. The outcome of our threat prevention procedure is a sugges-

tion of model attribute repair that eliminates threats. Whenever threat

prevention fails, we automatically explain why the threat happens. We

implement our approach using the state-of-the-art Z3 SMT solver and

interface it with the threat analysis tool THREATGET. We demonstrate

the value of our procedure in two case studies from automotive and smart

home domains, including an industrial-strength example.

1 Introduction

The proliferation of communication-based technologies requires engineers to have

cybersecurity in mind when designing new applications. Historically, security

decisions in the early stages of development have been made informally. The

upcoming requirements regarding security compliance in soon-to-be-mandatory

standards such as the ISO/SAE 21434 call for more principled security assess-

ment of designs and the need for systematic reasoning about system security

properties has resulted in threat modeling and analysis tools. One example of

this new perspective is the Microsoft Threat Modelling Tool (MTMT) [8], devel-

oped as part of the Security Development Lifecycle. MTMT provides capabilities

for visual system structure modelling. Another example is THREATGET [12,3],

a threat analysis and risk management tool, originally developed in academia

and following its success, commercialized and used today by leading word-wide

companies in automotive and Internet-of-Things (IoT) domains. Threat mod-

eling and analysis signiﬁcantly reduces the diﬃculty of a security assessment,

reducing it to accurate modeling of the systems and the security requirements.

Existing methods use ad-hoc methods to reason about the security of sys-

tems. As a result, it is not easy to extend such tools with capabilities like auto-

mated threat prevention and model repair. Although a trial-and-error method

is always possible, it does not provide a systematic exploration of the space

of possible prevention measures and leaves the question of optimizing the cost

arXiv:2210.03207v1 [cs.CR] 6 Oct 2022

of the prevention to the designer’s intuition. As a result, remedying a potential

threat remains cumbersome and simple solutions may be missed, especially when

multiple interacting threats exist.

This paper proposes a procedure for preventing threats based on a formal

model of the structure of the system and a logic-based language for specifying

threats. The use of rigorous, formal languages to model the system and specify

threats allows us to automate threat prevention. More speciﬁcally, we reduce the

problem of checking presence of threats in the system model to a satisﬁability

modulo theory (SMT) check. A threat speciﬁcation deﬁnes a class of potential

threats and a witness of a system model that satisﬁes a threat speciﬁcation

deﬁnes a concrete threat in the model. This allows us to frame the problem of

preventing concrete threats as an attribute parameter repair.

The attributes of system elements and communication links deﬁne a large

spectrum of security settings and, in presence of a threat, of possible preventive

actions. This class of repairs enables simple and localized measures whose cost

can easily be assessed by a designer. We formulate attribute repair as a weighted

maximum satisﬁability (MaxSAT) problem with a model of cost of individual

changes to the system attributes. This formulation of the problem allows us to

ﬁnd changes in the model with minimal cost that result in removing as many

threats as possible.

We introduce threat logic as a speciﬁcation language to specify threats. We

formalize the system model as a logic formula that consists of a conjunction of

sub-formulas, called assertions, parameterized by attributes that specify secu-

rity choices. The conjunction of the system model formula and a threat formula

is satisﬁable iﬀ that threat is present in the system. We introduce clauses that

change the speciﬁc instantiation of model attributes to a diﬀerent value and as-

sociate a weight with each such assertion. Then, the MaxSAT solution of this

formula is the set of changes to system model attributes with minimum cost that

ensure the absence of the threat. Given an incorrect system, we can choose the

weights so that we compute the set of changes to system model attributes with

the minimal cost to remove the existing threats from the model. To ensure that

our method scales to industrial size models, we also deﬁne a heuristic that pro-

vides partial threat prevention by addressing repairable threats and explaining

the reason why the others cannot be repaired. We believe that this method, even

though partial and approximate in general, can compute near optimal repairs

for many real-world problems.

We implemented the threat prevention method in the THREATGET tool

and evaluated it on two case studies from the automotive and the IoT domains.

Motivating Example We motivate this work with a smart home application

from the IoT domain, depicted in Figure 1. The smart home architecture con-

sists of 7typed elements: (1) a control system, (2) an IoT ﬁeld gateway, (3)

temperature and (4) motion sensors, (5) a ﬁrewall, (6) a web server and (7) a

mobile phone. The elements are interconnected using wired and wireless connec-

tors. The elements and connectors have associated sets of attributes that describe

their conﬁguration. For instance, every connector has attributes Encryption, Au-

thentication and Authorization. The attribute Encryption can be assigned the

values No, Yes and Strong. We associate to each attribute a cost of changing the

attribute value, reﬂecting our assessment of how diﬃcult it is to implement the

change. In this example, the temperature and the motion sensor communicate

wirelessly with the gateway. If the motion sensor detects a movement, the user

is notiﬁed by phone. It is possible to override the behavior, e.g., the heating can

be turned on remotely in case of late arrival. The web server protected by the

ﬁrewall allows for access and information exchange from and to the smart home.

The IoT sub-system protected by the ﬁrewall deﬁnes a security boundary called

the IoT Device Zone. Communication should be conﬁdential and encrypted out-

side the IoT Device, which is represented by the two associated assets.

IoT Field

Gateway

Motion

Sensor

Temprature

Sensor

Control

System Firewall WebServer Mobile

Phone

Cryptographic

Asset

Conﬁdentiality

Asset

Wireless

Connector

Wireless

Connector

Wire

Connector

Wire

Connector

Wire

Connector

Wire

Connector

Wireless

Connector

Wireless

Connector

Wireless

Connector

Wireless

Connector

IoT Device Zone

Fig. 1: Smart Home IoT model.

The potential threats that can be encountered in this smart home system

are characterized by logical relations between elements, connectors and their

attributes. Consider the two potential threats that are applicable to this example:

Threat 1: The web server enables data logging functionality without encrypt-

ing the data.

Threat 2: The mobile phone device is connected to the web server, without the

web server enabling data logging.

Assume that the web server has data logging enabled, but no data encryption,

thus matching Threat 1. If we consider this threat in isolation, we can repair

it in two ways: (1) by turning oﬀ the data logging, or (2) by implementing the

data encryption on the web server. The ﬁrst repair results in matching Threat 2.

Only the second repair results in the removal of all security threats. Given two

data encryption algorithms with costs c1and c2, where c1> c2, implementing

the latter is the cost-optimal option. We see that an optimal preventive solution

must consider simultaneous repair of multiple threats.

2 Threat Modelling

A threat model consists of two main components, a system model and a database

of threat rules. A system model provides an architectural view of the system

under investigation, representing relevant components, their properties, as well

as relations and dependencies between them 1.

System Model A system model Mconsists of:

–a set Eof elements: an element e∈Eis a typed logical (software, database,

etc.) or physical (ECUs, sensors, actuators, etc.) component.

–a set Cof connectors: a connector c∈Cis a direct interaction between two

elements, a source s(c)∈Eand a target element t(c)∈E.

–a set Aof security assets: an asset a∈Adescribes logical or physical object

(such as an element or a connector) of value. Each element and connector

can hold multiple assets. Similarly, each asset can be associated to multiple

elements and connectors.

–a set Bof security boundaries: a boundary b∈Bdescribes a separation

between logically, physically, or legally separated system elements.

–a set Aof attributes: an attribute a∈Ais a property that can be associated

to a system elements, connectors and/or assets. Each attribute acan assume

a value from its associated domain Da. We denote by v(x, a)the value of the

attribute aassociated to the element/connector/asset x. We ﬁnally deﬁne

an attribute cost mapping wx,a(v, v0)associated to (x, a)pairs that deﬁnes

the cost of changing the attribute value v∈Dato v0∈Da.

Given a system model M, we deﬁne a path πin Mas an alternating sequence

e1, c1, e2, c2· · · , cn−1, enof elements and connectors, such that for all 1≤i≤n,

ei∈E, for all 1≤i < n,ci∈C,s(ci) = ei, and t(ci) = ei+1 and for all

1≤i<j≤n,ei6=ej. We note that we deﬁne paths to be acyclic, since acyclic

paths are suﬃcient to express all interesting security threats.

We use the notation elements(π)and connectors(π)to deﬁne the sets of all

elements and of all connectors appearing in a path, respectively. The starting

and the ending element in the path πare denoted by estart(π) = s(c1)and

eend(π) = t(cn−1), respectively. We denote by P(M)the set of all paths in M.

Threat Logic We provide an intuitive introduction of threat logic for specifying

potential threats 2. The syntax of threat logic is deﬁned as follows:

ϕ:= R(X∪P)| ¬ϕ|ϕ1∨ϕ2| ∃p.ϕ | ∃x.ϕ

where X=E∪C∪A∪B,x∈X,Pis a set of path variables, p∈P, and

R(X∪P)is a predicate. The predicate R(X∪P)is of the form:

1The system and the threat model are formally deﬁned in Appendices A and B.

2The authors of THREATGET deﬁne their own syntax and semantics to express

threats [3]. We use instead predicate logic to facilitate the encoding of the forth-

coming algorithms into SMT formulas. Our implementation contains an automated

translation from THREATGET syntax to threat logic.

1. type(x) = t- the type of x∈Xis t;

2. xin p- the element or the connector x∈E∪Cis in the path p∈P;

3. connector(e, c)- the element e∈Eis either the source or the target of the

connector c∈C;

4. src(c) = e- the source of the connector c∈Cis the element e∈E;

5. tgt(c) = e- the target of the connector c∈Cis the element e∈E;

6. src(p) = e- the source of the path p∈Pis the element e∈E;

7. tgt(p) = e- the target of the path p∈Pis the element e∈E;

8. crosses(c, b)- the connector c∈Ccrosses the boundary b∈B;

9. contained(x, b)- the element or boundary x∈E∪Bis contained in the

boundary b∈B;

10. holds(x, a)- the element or the connector x∈E∪Cholds the asset a∈A;

11. val(x, att) = v- the valuation of the attribute att associated to x∈E∪C∪A

is equal to v.

Example 1. Consider a requirement that there exists a path in the model such

that all the elements in that path are of type Cloud. It is expressed with the

threat logic formula: ∃p.∀e.(ein p=⇒type(e) = Cloud).

We deﬁne an assignment ΠMas a partial function that assigns element,

connector, asset, security boundary and path variables to concrete elements,

connectors, assets, security boundaries and paths from the system architecture

model M. We denote by ΠM[x7→ i]the item assignment in which xis mapped

to iand otherwise identical to ΠM. Similarly, we denote by ΠM[p7→ π]the

path assignment in which pis mapped to πand otherwise identical to ΠM. The

semantics of threat logic follow the usual deﬁnitions of predicate logic.

We say that a threat logic formula is closed when all occurrences of element,

connector, asset and security boundary variables are in the scope of a quantiﬁer.

Any closed threat logic formula is a valid threat speciﬁcation. Given a system

model Mand a closed threat logic formula ϕ, we say that Mwitnesses the threat

ϕ, denoted by M|=ϕiﬀ ΠM|=ϕ, where ΠMis an empty assignment.

From Threat Logic To First Order Logic (FOL) We observe that we inter-

pret threat logic formulas over system models with a ﬁnite number of elements

and connectors, and hence we can eliminate path quantiﬁers by enumerating the

elements and connectors in the path. By eliminating path quantiﬁers, we obtain

an equisatisﬁable FOL formula that can be directly used by an SMT solver.

The path quantiﬁer elimination procedure Tthat takes as input a threat for-

mula ϕand computes the equisatisﬁable ﬁrst-order formula T(ϕ)is formalized

in Appendix 5.

Example 2. We formalize the two threats described in Section 1:

Threat 1 ∃e.(type(e) = WebServer ∧val(e, Data Logging) = Yes)

∧val(e, Data Encryption)6=Yes)

Threat 2 ∃p, e1, e2.src(p) = e1∧tgt(p) = e2∧

type(e2) = WebServer ∧type(e1) = MobilePhone

∧val(e2,Data Logging)6=Yes)

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

ThreatRepairwithOptimizationModuloTheoriesThorstenTarrach1,MasoudEbrahimi2,SandraKönig1,ChristophSchmittner1,RoderickBloem2,andDejanNickovic11AITAustrianInstituteofTechnology2GrazUniversityofTechnologyAbstract.Weproposeamodel-basedprocedureforautomaticallypre-ventingsecuritythreatsusingformalmodels....

展开>> 收起<<

Threat Repair with Optimization Modulo Theories Thorsten Tarrach1 Masoud Ebrahimi2 Sandra König1 Christoph.pdf

共27页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Threat Repair with Optimization Modulo Theories Thorsten Tarrach1 Masoud Ebrahimi2 Sandra König1 Christoph

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: