0Array 14 (2022) 1001460//creativecommons.org/licenses/by/4.0/)。0ScienceDirect提供的内容列表0数组0期刊主页：www.elsevier.com/locate/array0通过对用户行为进行形式建模生成用户特定安全策略来增强网络安全0Arwa AlQadheeb a，Siddhartha Bhattacharyya a，�，Samuel Perl b0a 佛罗里达理工学院计算机工程与科学，墨尔本，FL，32901，美国 b卡内基梅隆大学软件工程研究所，匹兹堡，PA，15213，美国0文章信息0关键词：零信任 自动验证 正确性网络安全策略 安全策略 形式方法 用户行为自动化安全策略生成 有限状态自动机定时计算树逻辑0摘要0当今组织面临着一个艰巨的挑战，即在拥抱新兴技术的同时保护支持关键业务功能的系统和数据。尽管安全执行技术取得了重大进展，攻击者仍然能够compromi组织并访问。计算机入侵的影响变得如此不可持续，以至于许多组织都在彻底重新思考其内部网络安全的方法。这种方法被称为零信任，它试图消除对受信任的内部网络边界的所有概念。零信任的好处包括显著增加攻击者实现其目标所需的工作量。但零信任也将增加内部安全团队的管理复杂性。这些团队需要一种收集数据并基于分析做出策略决策的方法。这个过程需要对所有组织系统和数据进行，而且需要在所有访问上下文中进行。我们的方法使用形式方法来对最终用户的安全相关行为进行建模和检查。研究人员发现，用户的安全决策与诸如人口统计学、个性特征、决策风格和风险偏好等因素相关。我们使用有限状态自动机（FSA）来描述这些行为。这允许基于定时计算树逻辑（TCTL）自动制定线性时间安全属性。然后使用逻辑来检查收集和观察到的安全行为对策略的满意程度。这种形式行为分析可以与上下文分析过程中的其他安全和网络数据相结合，这需要对每个零信任访问请求进行。其他网络或主机安全数据可能包括地址标识符、令牌、事件数据、数据包检查、运行进程数据、网络威胁情报等等。我们的方法允许拥抱零信任理念的组织生成特定上下文的安全策略，并可以自动验证其正确性和完整性。01.介绍0当今组织面临着一个艰巨的挑战，即在拥抱新兴技术的同时保护支持关键业务功能的系统和数据。尽管安全执行技术取得了重大进展，攻击者仍然能够compromise组织并访问。也许比以往任何时候都更多，组织需要拥抱包括物联网、机器学习和统计分析以及云计算在内的新技术创新。随着这些新设备和服务的推出，组织有将它们连接到其业务网络的业务需求。如果他们不这样做，他们就有可能被竞争对手在市场上超越。这进一步测试了他们的安全团队防止0� 通讯作者。邮箱地址：sbhattacharyya@fit.edu（S.Bhattacharyya）。0新的入侵是难以预测的，因为攻击面迅速变化，软件供应链变得越来越复杂。安全专业人员正在开发新的安全模型，以更好地准备预防、检测、应对和恢复网络攻击。0https://doi.org/10.1016/j.array.2022.1001462021年6月10日收到；2022年2月15日收到修订稿；2022年4月1日接受。20Array 14（2022）1001460A. AlQadheeb等人。0心理学研究表明，人类的信息处理能力有限，他们依赖以往的经验来采取未来的行动，这可能妨碍他们的安全选择。0大多数计算机系统都是基于一般认知设计的。0大多数计算机系统都是基于一般认知设计的。0著名黑客凯文∙D∙米特尼克表示，最有效的入侵技术是利用人类作为系统中最薄弱的环节。从他的观点来看，克服这个问题0著名黑客凯文∙D∙米特尼克表示，最有效的入侵技术是利用人类作为系统中最薄弱的环节。从他的观点来看，克服这个问题的唯一可靠方法是将安全技术与严格的安全政策结合起来，并为用户提供适当的教育计划和培训课程。0我们的方法演示了基于形式方法的框架使用0生成用户特定安全策略的工作，为现有文献做出了新的贡献。0本研究的其余部分组织如下：第2节0更深入地描述了相关工作。第3节介绍了研究方法论，概述了自动化方法的顺序开发过程。第4节讨论了用户安全行为的选择。第5节讨论了模型考虑因素和所选的建模范式。第6节讨论了在第6.1节中选择和建模安全行为的整体实验，第6.2节解释了检查用户安全行为满意度的过程。第6.3节定义了生成用户特定策略的规则。第7节讨论了使用我们框架获得的最终结果。最后，第8节阐明了我们的结论和未来工作。02. 相关工作0基于形式方法的方法已被应用于建模0对用户行为进行分析，并使用认知架构中的用户模型进行建模，正如Curzon[8]所描述的那样。通过这种方法，研究人员能够捕捉设备和人类之间潜在的错误交互。Curzon的研究重点是0人类认知的建模遵循认知原理。这些形式模型是使用定理证明器进行验证的，而不是模型检查器。因此，它比模型检查器使用的自动化方法更加手动化。最后，Curzon的工作讨论了一种验证方法，但没有实施这种方法。Degani[9]讨论了在航空电子领域中对人机界面进行形式建模和分析以捕捉界面设计中的错误的方法。一旦用户模型被开发，就会开发一张对应表来理解用户对事件的反应。最后，通过生成用户模型与自动驾驶仪模型的掩码同步乘积来开发组合模型。这项工作也是一项理论研究，没有使用任何工具进行实施。Bolton[10]调查了基于形式验证的方法，该方法被应用于验证人机交互以识别界面设计中的错误。但是，所有这些方法都集中在应用形式方法来在设计时识别错误，没有一种方法讨论了如何将形式用户模型作为分析实时数据的一部分，以及用于网络安全的安全策略生成。我们的方法演示了如何对用户的形式建模的网络安全行为进行实时分析，然后生成安全策略。Houser[11]讨论了开发心理用户模型来捕捉用户认为系统当前状态是什么，实际系统状态是什么，然后识别是否存在任何漏洞。Houser的模型并没有捕捉到用户实际表现的行为，而我们通过审查Egelman[12]进行的研究中用户表现的安全和不安全行为来进行建模，这可以用于生成安全策略。类似的工作是Enoch, SimonYusuf的“动态网络安全建模与分析。”（2018）[1]。Enoch使用网络状态输入来生成基于约束的可适应安全模型。动态网络状态的变化被用作输入来生成修改后的图形安全模型，但并没有明确采用用户行为输入。该工作还针对的是一个可以动态调整网络配置的网络（也称为主动防御），而不是假设零信任环境。用于生成和评估攻击场景的模型侧重于可能的攻击者行为（攻击树），而不是评估最终用户行为、选择和设备设置的风险。0更具体地应用于零信任环境的四项用于生成策略的额外工作。Chen,Baozhan等人[13]和Mandal,Sudakshina等人[14]都专注于动态生成访问控制决策，但在决策过程中，没有明确包括最近的用户安全行为、选择或设备设置作为输入或模型特征。Eidle,Dayna等人[15]通过防火墙访问控制列表（ACL）和认证网关动态调整8个不同信任级别的访问策略。该模型以来自防火墙、认证网关和其他网络设备的警报数据作为输入，但不包括最近的用户安全行为，这些行为不会触发警报。最后，Dean,Erik等人[16]在零信任环境中在会话认证过程中使用自动设备健康验证结果作为部分用户设备的输入。这对应于设备保护和更新的属性，甚至可能对密码或主动意识进行映射。然而，该工作没有列出在“健康检查”中执行的特定设备参数检查。另一个关键区别是，该工作没有使用可达性分析来应用不同级别的安全权限，以适用于略微更高风险但仍然可接受的设备配置。03. 研究方法0研究方法描述了解决问题所使用的方法。0生成遵循零信任理念的用户特定安全策略的问题。30数组14（2022）1001460A. AlQadheeb等人0图1. 研究方法。0我们的方法利用了对人类意图、态度、规范以及由此产生的网络安全决策行为的研究结果。有许多研究表明可用安全性是一个难题。用户经常忽略明确的警告，并误解许多风险及其造成的影响的可能性[17]。用户也会理性地拒绝警告，因为他们在过去的经验中经历了太多的虚假警报[18,19]。人与计算机的交互界面很难设计，固有的认知弱点可能会对安全决策产生负面影响[3,20]。一些研究发现，基于背景、文化和态度提出安全决策时，个体用户的行为会有所不同[2,5,21]。由于人类行为多种多样，难以预测且开放式，我们将我们研究中的安全行为限制在先前研究中已经验证的具有现有量表的行为。Egelman和Peer创建了一个安全行为意图量表（SeBIS）[12]，用于评估用户根据自我声明的信息遵守计算机安全建议的能力。该量表侧重于四个构建，即设备保护、密码生成、主动意识和更新。Gratian等人[2]证实了SeBIS的准确性，并扩展了SeBIS以研究个性特征和人口统计学与安全意图的相关性。我们在图1中的形式化方法引导的用户特定策略生成框架（FMUSPGF）中设置了整个研究的结构，该图显示了开发过程作为四个阶段的序列。FMUSPGF的第一步涉及选择安全行为，这是通过对现有文献进行调查来实现的，以确定预期的安全行为。一旦选择了安全行为，第二步涉及对这些行为进行建模，我们采用了基于形式化方法的方法。在对安全行为进行建模后，下一步涉及对安全行为进行标记，这是通过执行使用形式化规范设计的查询来完成的。最后，根据前一步中的标记生成用户特定的安全策略。我们的主要贡献在于设计了一个基于形式化方法的框架，以支持网络安全的用户特定策略生成过程。在这个过程中，我们演示了如何识别和选择定义用户安全行为的基本特征。然后，我们将已识别的安全行为建模为形式化模型，以实现自动推理。最后，我们能够检测用户安全行为中的弱点，然后提出相关的策略。04. 选择安全行为0在本节中，我们专注于通过考虑用户所做的安全决策来选择用户的安全相关行为。它描述了数据收集、比较和选择的范围，以构建可靠的知识库，代表了开发正式模型的要求，我们在审查了广泛的可能性后完成了这一目标。先前的研究全面调查了人口统计学、个性特征、决策风格和冒险偏好的个体差异与其影响之间的相关性0表1 [5]和[2]心理测量的比较0度量研究[5] 研究[2]0考虑未来后果（CFC）� � 安全行为意图量表（SeBIS）� � 领域特定风险态度（DoSpeRT）� �国际人格项目池（IPIP）� � 普通决策风格（GDMS）� � 巴拉特冲动量表（BIS）� �认知需求（NFC）� �0在网络空间中用户安全相关行为的研究。我们选择关注决策，因为实验证明它比人口统计学、个性特征和冒险倾向更能预测安全实践[2,12]。本研究的预测因子选择源自两个早期研究的观察，分别由Egelman和Peer[5]以及Gratian等人[2]进行。这两项研究旨在开发定制的安全防御措施，考虑个体差异，以限制用户的错误及其后果。[2]的样本人群包括来自美国一所大型公立大学的高等教育参与者，而Egelman和Peer调查了一群年龄超过18岁的亚马逊机械土耳其（MTurk）的个体。他们都使用SeBIS进行研究；然而，Egelman和Peer关于安全的兴趣是调查SeBIS与决策心理测量之间的相关性。Gratian等人对[5]进行了扩展版本，以证实SeBIS的准确性，拓宽了SeBIS的使用范围，以检验个性特征和人口统计学与安全意图的相关性。从表1比较Egelman等人[5]和Gratian等人[2]，我们确定SeBIS、DoSpeRT和GDMS用于识别安全意图、冒险倾向和决策制定之间的关系。确定如何对特定情况做出反应的过程需要风险评估，考虑未来后果，并探索可能的替代方案。人类心理的自然结构、人类信息处理能力的限制以及他们几乎绝对依赖于以前的经验，阻碍了做出正确选择[3]。未能确定什么是正确的事情，反之亦然，在网络安全中是一个重要问题。如果有些人决定在公共场所不看管他们的设备，设置容易猜测或破解的密码，匆忙下载匿名电子邮件附件，或低估软件更新的重要性，他们更容易成为狡猾个体的受害者。我们考虑将每个用户的行为建模为一系列不同连接的决策。每个决策与特定的SeBIS构建相关：设备保护、密码生成、积极意识或更新。我们选择使用Egelman和Peer的研究结果来开发正式的用户安全相关行为，因为这些行为被确定为现实和用户安全行为。40Array 14（2022）1001460A. AlQadheeb等0图2.网络安全用户行为知识表示架构。05.建模用户安全行为0在审查与安全行为相关的决策过程的研究后，建立了适当的知识库，并选择了最相关的用户行为来开发形式模型。本节的内容侧重于有关架构抽象级别和所选建模范式的设计选择。05.1.设计选择：抽象级别0模拟人机交互是具有挑战性的，因为人类行为的复杂性和广泛的知识要求。尽管我们选择了特定的知识库，但模拟和检查与设备保护、密码生成、主动意识和更新相关的用户安全行为的每个方面仍然具有挑战性。为了模拟SeBIS不同方面的用户行为，我们应用了从软件/系统工程中继承的分解原则来构建模型的结构。模拟关于安全行为的知识的架构包括不同层次的抽象，以便于调试，增加可读性/可维护性并减少复杂性。我们将结构分解为不同类型的安全服务，从（1）作为最抽象的层次开始，到（3）作为最低抽象级别结束。通过这样做，我们消除了关于我们为特定SeBIS维度使用了哪些安全方面的混乱。在这里，我们详细说明每个抽象级别。0•第（1）层是四个安全服务检查层中最抽象的一层。它吸收了SeBIS概念：设备保护、密码生成、主动意识和更新，这些是Egelman和Peer指定的。这些对应于需要执行的安全任务的最高级别表示。•第（2）层根据第1级中确定的每个类别的关键参数来分解SeBIS概念，例如设备保护、更新机制、密码方法以及对威胁和违规行为的关注。然后，根据用户对他们想要采取的行动的决定，进一步分解为可能的附加子服务。•第（3）层有一个子树，从第2层的具体内容下降，例如用于设备保护的屏幕锁定功能，并由用户选择启用。05.2.设计选择：建模范式选择0尽管有几种方法可以用来建模用户行为，比如马尔可夫链、体系结构表示，但我们选择了基于形式方法的方法。我们决定最适合表示用户行为的方法是使用有限状态自动机（FSA）[22]，因为它允许我们在设计阶段早期进行自动化分析，这样我们就可以推理用户行为的逻辑表示，以评估替代设计选项是否存在深远的影响。它还允许以图形方式轻松可视化用户行为。它还可以使用定义良好的工具。为了选择正确的平台来设计和检查满足形式验证用户行为的形式模型，仔细考虑了NuXMV[23]、Uppaal [24]、PVS [25]和Z3 [26]等几种形式。我们选择了Uppaal[27,28][24]，因为它能够模拟对网络安全至关重要的时间方面，以及它能够生成和可视化反例。Uppaal将模型表示为定时自动机，Uppaal形式主义支持使用时间逻辑对网络定时自动机进行模型检查。这种建模范式允许将需求作为时间逻辑查询的执行，以彻底检查相关安全属性的满足情况。接下来我们描述Uppaal使用的定时自动机形式主义。05.2.1.时态自动机中的数学表示。Uppaal使用时态自动机[29]，作为建模形式的混合自动机的子集。在设计人机交互时的一个基本要求是能够模拟与操作或规则执行相关联的时间。时态自动机是有限自动机，扩展了有限实值时钟的有限集。在自动机内的转换的守卫中使用时钟或其他相关变量的值。根据守卫评估的结果，转换可能启用或禁用。变量可以被重置并作为状态的不变量实现。使用时态自动机方法对时态系统进行建模是符号化的，而不是显式的。它允许根据需要考虑无限状态空间的有限子集（即，使用依赖于安全性属性和时态自动机的等价关系的区域自动机），这称为区域自动机。还存在各种工具来输入和分析时态自动机和扩展，包括模型检查器Uppaal和Kronos[30]。0• 时态自动机（TA）时态自动机是一个元组(�, �0, �, �, �,�)，其中：�是位置的集合；�0 ∈�是初始位置；�是时钟的集合；�是动作、共动作和不可观察的内部动作的集合；���×�×�(�)×2�×�是位置之间的边的集合，带有50Array 14 (2022) 1001460A. AlQadheeb等人0动作、守卫和要重置的一组时钟；�∶�→�(�)为位置分配不变量。我们将时钟估值定义为函数�∶�→R≥0，从时钟的集合到非负实数的集合。让R�为所有时钟估值的集合。对于所有�∈�，�0(�)=0。如果我们将守卫和不变量视为时钟估值的集合（稍微放松形式），我们可以说�∈�(�)表示�满足�(�)。0• 时态自动机语义0设(�, �0, �, �, �, �)是一个时态自动机��。��的语义被定义为一个带标签的转→�，其中��� × R�是状态的集合，�0 = (�0, �0)是初始状态，→�� × {R≥0 �是转换关系，使得：01. (�, �) → � (�, � + �)，如果 ��′: 0 ≤ �′ ≤ � � � + �′ ∈ �(�) 2. (�, �) �, �, �′) ∈ �，使得� ∈ �，0� = [� � 0]�且�′∈�(�)0对于 � ∈ R ≥ 0，� + � 将�中的每个时钟�映射到值�(�) + �，并且[� �0]�表示时钟估值，将�中的每个时钟映射到0，并在���上与�一致。请注意，�时钟的简单条件，它们使得从一个位置到另一个位置的转换（或边�）成为可能；除非发生相应的动作�，否则不会执行启用的转换。类似地，边�的重置时钟�指定了在边上执行转换时将值设置为零的时钟。因此，时态自动机是带有重置和条件的有限有向图，这些条件是关于非负实值时钟的。然后，时态自动机可以组合成一个时态自动机网络，其中包括一组共同的时钟和动作，由�个时态自动机��� = (��, �0, �, �, ��, ��)，1 ≤ � ≤�。这使我们能够检查在时态自动机网络上表达的可达性、安全性和活性属性，这些属性用时态逻辑表达。时态自动机的执行，用����(��)表示，是连续转序列，而��的执行轨迹集合用������(��)表示。05.3. 用于验证的查询语言0Uppaal中的验证过程使用特定类型的查询语言，用于指定需要检查的一组属性。查询语言是计算树0Uppaal中的验证过程使用特定类型的查询语言，用于指定需要检查的一组属性。查询语言是计算树逻辑（CTL）的子集，称为定时CTL（TCTL）[ 31]。定时计算树逻辑的语法如下所示：0Uppaal中的验证过程使用特定类型的查询语言，用于指定需要检查的一组属性。查询语言是计算树逻辑（CTL）的子集，称为定时CTL（TCTL）[ 310• � 是属性或命题 • a 是原子动作。 • g 是时钟约束。 • E表示‘‘对于某些路径’’。 • A表示‘‘对于所有路径’’。 • J 是边界为自然数的区间。• state � � � E( � 1 ∪ � � 2 ) ‘‘对于某条路径’’ � � , � � +1 ...0• , � � +1 ...0( � k ≥ i, k-i ∈ J) (( � � � q) ( � j, i ≤ j < k)( � � � p))0TCTL类似于CTL，具有时间连接词0表示为符号对。其中，对中的第一个元素表示路径量词之一，即 A 或 E，而对中的第二个元素是以下之一：0• G 表示‘‘路径中的所有状态’’。 •F 表示‘‘路径中的某些状态’’。0路径公式和状态公式的不同组合0Uppaal接受的查询包括： AG 不变式 A[] ， EG 可能总是 E[] ， AF 最终 A<> ， EF 可能 E <> 。06. 实验0进行实验的第一步是实验0建立模型的过程涉及在时态自动机中对所选安全行为进行建模 6.1。一旦模型开发完成，下一步就是进行实验（ 6.2）来标记良好和不良的安全行为。06.1. 实验设置：建模选定的安全行为0我们模型的设计是由能力指导的，以便0检查TCTL中良好和不良用户安全行为的存在（根据学术文献中的工具进行测量）。第 6.1.1 到 6.1.4节将进一步说明我们为什么以及如何选择了不同安全设置中最关键的问题，这些问题是设备安全、密码生成、主动意识和更新的一部分。利用现有文献中的行为测量标准，我们设置了一些示例，将良好的决策与不良决策分开。0在这项工作中，我们手动进行数据收集，以展示0概念，但是仪器的细节（或数据收集实施）将根据组织及其零信任解决方案、设备、政策和流程而变化。对于实施零信任策略决策，也有不同的建议解决方案，任何用户安全行为的数据收集或测量都需要与特定的零信任解决方案进行交互。零信任解决方案概念上包括策略执行点和策略引擎。通常，安全决策所需的数据是由策略执行点收集并发送到策略引擎进行审查。组织可以添加数据收集代理，以根据其特定的实施和政策包括端用户安全行为。我们的方法允许拥抱零信任理念的组织生成特定上下文的安全策略，这些策略可以自动验证正确性和完整性。未来的工作将需要将用户特定的安全行为数据添加到现有数据中，这些数据被馈送到策略引擎。零信任环境通常设想为策略引擎分析网络、应用程序、设备和数据访问策略，并在访问上下文中做出决策。一些示例包括使用网络或主机安全数据，包括MAC地址标识符、InternetProtocol（IP）地址标识符、安全访问令牌、会话令牌、进程事件数据、数据包检查数据、运行进程数据、威胁情报数据、设备特定数据，如已安装的应用程序清单、配置设置、安全相关设置等等。06.1.1. 设备安全0• 设备保护0我们选择设备保护作为设备安全性的第一个标准。这意味着用户是否通过密码、PIN码、指纹或图案来保护他们的设备。尽管锁定各种设备是一个简单的安全任务，但有时会被最终用户低估。在2017年进行的皮尤研究中心调查中，28%的美国手机用户报告说他们不使用PIN码或任何其他安全功能来访问他们的智能手机[ 32]。这种安全问题在工作环境中更为关键。例如，如果一些员工在工作场所之外使用便携设备（如笔记本电脑、平板电脑或智能手机）作为他们的主要工作电脑，他们可能会在一些地方（如酒店房间或汽车）不保护设备。这样一来，如果他们的设备被盗，它已经是解锁状态，公司的数据将落入未经授权的个人手中。大多数组织要求对持有其数据的设备进行此项控制，但在所有生态系统和设备中进行监视和执行可能很困难。60数组14（2022）1001460A. AlQadheeb等0图3. 设备安全状态转换图。0表2 设备安全性属性。0知识库属性编号01 E <>（device_protection.enabled） 2 E<>（device_protection.disabled） 3 E<>（screen_locking.turned_on） 4 E<>（screen_locking.turned_off） 5 E<>（timeout.short） 6 E <>（timeout.long）0• 屏幕锁定密码保护的屏幕保护程序功能是指在一段时间的不活动后自动关闭设备。一些最终用户发现当他们不得不在超过超时时间时一直登录时，这是一件有点麻烦的事情。其他人对威胁的认识较低；他们认为由于他们几乎一直在他们的便携设备周围，尤其是智能手机[ 33]，所以不会出什么问题。还有一些人设置了密码保护的屏幕保护程序，但他们调整了默认的超时时间（即通常为15分钟）为更长的时间[ 34]。我们研究设备安全的这一方面，是因为不设置密码保护的屏幕保护程序将允许恶意个人（例如内部威胁）访问数据或执行一些他们无权查看或执行的任务[ 35]。内部威胁是最困难的安全问题之一；恶意内部人员可能会给组织带来比外部人员更大的风险，因为他们对安全基础设施、实践和漏洞更熟悉。他们可以更容易地避开检测，并长时间地保持隐藏。在表2中，我们可以看到我们如何将上述标准转化为TCTL公式，而图3则描述了设备保护、屏幕锁定和屏幕锁定超时状态转换图。06.1.2. 密码生成 • 密码年龄密码在网络安全中是一个长期存在的问题。人们提出了许多建议，并执行了政策，但弱密码问题仍在不断增长。设置最大密码年龄是维护适当密码卫生的传统技术之一。它要求用户定期更改密码，通常在30到90天之间[ 36]。有人可能会认为定期更改会使密码更难记住，因此更有可能被不安全地存储。我们将这条规则包含在我们的规范集中，以展示可以包含在知识库中的标准的一个例子。0用户记住的密码越短，就越有可能被不安全地存储，因此更有可能被不安全地存储。用户正在调整和发展应对这一负担的应对机制，通过对当前密码进行一些修改。我们将这条规则包含在我们的规范集中，以展示可以包含在知识库中的标准的一个例子。 • 密码长度人们想要保护自己的个人信息，但他们不愿意为此付出更多的努力。最大的例子是，尽管不断有关于使用弱密码和由此行为造成的严重后果的安全警告，但他们仍然使用短而容易记住的密码。根据密码心理学报告，参与研究的47%的人宣称他们更喜欢选择简单的密码，因为他们害怕忘记它们[ 37]。Martin等人（2012）说明，通过暴力破解攻击猜测密码最有可能不会成功，而长且复杂的密码包含大小写字母、数字和符号。他们提到，破解长度为4、8或16个字符的复杂密码分别需要大约81秒、210年和1.4万亿年[ 38]。根据Maddox和Moschetto（2019）的说法，当用户为某个账户分配密码时，他们应该保持足够的长度，避免常见的字符替换，并使用各种字母、数字和特殊字符[ 39]。我们认为密码的长度是必要的，以便识别那些账户容易受到密码攻击的人。 • 密码可重复使用面对如此多的账户需要处理和跟踪，用户可能会诱惑着在所有账户上使用相同的密码，给自己带来一些安心；用户可能会后悔。为多个网站重复使用相同的密码比在一张纸上分别写下不同的密码带来更大的风险。如果个人决定为他们的不同账户分配一个密码，他们将允许攻击者侵入使用相同密码的其他账户[40]。密码保护的挣扎在于，大多数最终用户承认密码重复使用的风险和后果；然而，35%的人忽视这一知识，而更喜欢记住他们容易和熟悉的密码[ 37]。我们选择涵盖密码生成的这一方面，因为在最坏的情况下，由此产生的风险不仅限于最终用户，而且还延伸到工作场所和同事，如果他们将工作密码重复用于其他个人账户。70Array 14 (2022) 1001460A. AlQadheeb et al.0表3 密码生成属性。0No. Knowledge base property01 E <> (密码年龄.未过期) 2 E <>(密码年龄.已过期) 3 E <> (密码长度.长) 4 E <>(密码长度.短) 5 E <> (密码可重用性.未使用) 6 E<> (密码可重用性.已使用)0表3列出了Uppaal规范语言中密码年龄、长度和可重用性的等效表达。06.1.3. 积极意识0• 发现威胁迹象0毫无疑问，人们对网络安全的兴趣正在增长和扩大，使人们更加了解和谨慎地对待在线信息共享、虚假电子商务网站、诈骗和安全威胁。在这个不完美的世界中总是有一个“但是”，因为有相当数量的人缺乏数字安全意识和教育，这反过来影响了他们识别威胁的能力，即使有明显的迹象。如果最终用户无法发现设备上的间谍软件迹象、识别社交工程尝试、识别钓鱼或欺骗邮件，或者其他任何隐匿的活动，他们将无法保护自己免受身份盗窃的侵害。根据Verizon的数据泄露调查报告(DBIR)(2019)，钓鱼攻击是数据泄露的主要原因之一。它是32%的确认数据泄露的原因，以及78%的网络间谍活动事件[41]。基于此，我们强调了在为时已晚之前调查用户识别和避免钓鱼诈骗的重要性。0• 报告威胁0在“如果你看到了什么，请说出来®”全国宣传活动中，该活动提高了公众对恐怖主义相关犯罪指标的认识，我们被鼓励如果发现有什么不太对劲的事情就向当局报告，以确保自己和我们的社区的安全[42]。在组织环境中也是如此；报告可能的安全事件可以在入侵检测的早期阶段节省宝贵的时间[43]。如果员工了解网络攻击的类型以及它们的外观和发生方式，他们更有可能注意到系统上发生的未经授权的变化。他们可能会更有信心并愿意联系IT部门。缺乏网络安全意识、培训和警惕性，以及员工与IT团队之间的沟通不畅，会使前者犹豫不决，并质疑自己是否真的发现了什么。我们将这一研究领域纳入到我们的研究中的想法是为了模拟用户到底是真的教育不够，还是只是太鲁莽而不报告这样紧急的事情。0• 政策合规0识别、确定和处理对组织资产机密性、完整性和可用性的风险是头等大事。安全政策和程序是任何组织管理控制层次结构的一部分，以维护敏感数据的安全，这是最关键的资产，免受复杂和不断发展的威胁环境的影响。对任何组织来说，最大的担忧之一是如何保护数据免受员工的侵害[44]。制定安全政策和指南是为了告诉员工在与信息系统互动时什么是可以接受的，什么是不可以接受的。问题在于员工的不合规行为[45]。根据Mutlaq等人(2016)的说法，不合规行为可能是0表4 积极意识属性。01 E <> (发现威胁迹象.是) 2 E <>(发现威胁迹象.否) 3 E <> (报告威胁.是) 4 E<> (报告威胁.否) 5 E <> (安全策略遵守) 6 E<> (安全策略违反)0分类为：首先，是有意或计划的行为，旨在损害组织实体的异常行为。其次，是违反安全策略但没有恶意造成损害的疏忽行为。第三，是由于缺乏网络安全知识和培训而产生的无知行为。在确定安全策略违规的不同解释后，我们对终端用户对安全策略的遵守进行了建模，因为这有助于确定对特定用户施加的正确策略行动。表4显示了已生成的线性时间属性，用于研究积极意识的知识库方面。06.1.4. 更新0• 更新机制0与安全相关的软件更新是终端用户应该更加关注并确保定期安装的最重要的安全保护工具之一。终端用户可以配置操作系统和应用程序更新的几种选项，例如更新是如何下载和安装的（即自动还是手动）在他们的设备上。大多数现代软件系统都设置为自动下载和安装安全和其他必要的更新，无需人类做出决定。相反，手动更新允许用户更好地控制他们的设备，选择安装哪个更新以及何时安装。我们选择包括用户对更新机制的偏好，以观察不同的行为。0• 更新时间0尽管一些软件更新和补丁是为了解决先前安装的软件中发现的安全漏洞，但一些终端用户避免或延迟安装，因为他们认为这些增量更新只是无用的技术添加[46]。在此存在着那些在可用一段时间后才手动下载和安装更新的用户的风险。我们从中看出，延迟安装最新更新和补丁会为恶意个体利用用户设备上的开放安全漏洞创造机会窗口[47]。因此，我们进一步调查了用户对及时更新的疏忽行为的特征和建模。0• 重启时间0软件开发人员不断努力改进安全性，通过将用户角色排除在软件更新周期之外。他们发现用户干预仍然是必要的，因为一些更新需要设备重新启动才能使更改生效[48]。有一些操作系统，如微软Windows，开发出警告用户如果更新安装后需要重新启动。在这种情况下，系统会弹出通知窗口，说明将在一段时间内重新启动（通常为10分钟）。80数组14 (2022) 1001460A. AlQadheeb等人0表5 更新属性。0知识库属性编号01 E <> (更新机制.自动) 2 E <> (更新机制.手动) 3 E <>(更新时间.短) 4 E <> (更新时间.长) 5 E <>(立即重启时间) 6 E <> (一段时间后重启)0用户可以选择立即重新启动设备或延迟一段特定时间。如果用户选择延迟，警告对话框将再次显示相同的选项[48]。用户延迟重新启动任务，因为他们可能有一些紧急事务使他们无法在几个小时内重新启动。多次推迟重新启动的决定可能会对设备的安全性产生负面影响，因为对于计算机系统来说，更新安装尚未完成。我们观察了更新的这一方面，以引起疏忽和无知用户对立即重新启动的重要性的注意。在表5中，我们提供了用定时时态逻辑TCTL表达的更新的正式规范。06.2. 实验：对安全行为进行分类0在本节中，我们使用不同的安全测试案例对几种不同的安全0行为，作为有限状态自动机（FSA）。对于每个单独的测试案例，我们生成一组特定于用户的线性时间属性。然后根据可达性分析的结果将行为分类为良好或不良。一旦行为被分类，我们生成相关的安全权限，如严格、中等和最不限制。06.2.1. 自动化分析0我们试图分析用户的行为，以便进行仔细的0分析并揭示他们对安全系统产生重大影响的不良安全决策。为了最终实现我们的目标，我们设计了六个测试案例，涵盖了围绕设备保护、密码生成、主动意识和更新的真实场景中用户表现出的不同安全行为。对于每个测试案例，我们使用Uppaal工具将用户的行为表示为状态转换图，手动生成特定于用户的线性时间属性，应用可达性分析，识别良好和不良的安全行为，并生成特定于用户的策略。在本节中，我们演示了这些测试案例的一个示例，作为我们基于形式方法的方法的说明。06.2.2. 代表测试案例0为了获得可靠的测试案例，我们必须进行多次0假设和预测某些用户可能的行为和安全相关决策。在一个测试案例中，我们创建了一个名为Tom的用户的场景，他在一家网络营销公司担任数据录入专员。Tom被分配一台笔记本电脑，用于直接与公司业务相关的工作，并允许他在规定工作时间之外远程工作。基于此，公司要求他负责并采取合理预防措施来保护和维护笔记本电脑及其内容。对于这项研究，我们专注于捕捉Tom的安全行为而不是他的系统角色。图4代表了Tom安全相关行为的状态转换图。所有其他模型都可以在https://github.com/sbhattacharyya/USPGZeroTrust找到。01 有限状态自动机（FSA）的建模、验证和验证的集成工具环境[24]。06.2.3. 生成特定用户的安全属性0在前一节中，我们成功地对0用户的安全相关行为，通过有限状态自动机（FSA）的建模图展示。我们让Tom展示了关于设备保护、密码生成、主动意识和更新的不同良好和不良的安全行为。为了自动分析Tom的行为，我们需要手动创建针对Tom生成的线性时间属性。在图5中，我们生成了我们需要检查的属性，这些属性是基于第4节中指定的先前识别的属性生成的。我们生成这些属性是为了区分Tom未能应用适当的安全实践的方面。06.2.4. 可达性分析0使用模型检查进行可达性分析是一种验证过程0为基于状态转换概念设计的模型。根据Kong等人（2015）的说法，可达性分析是一种在状态转换系统中使用的技术，用于找出可以通过特定系统模型访问的状态的类型和数量[49]。可达性分析允许验证、验证和检查性能指标的形式分析，如下所述：0• 验证：显示了模拟过程，其中展示了模型0应反映其意图。0指标。0规范是否符合构建的模型。0• 验证：进行检查过程以确保规范符合构建的模型。0是由图形匹配方法。0在这些过程中，我们正在检查我们的满意度0规范（即属性）在用户行为模型的任何、一些或所有状态中。根据Eleftherakis等人（2001）的说法，“模型检查器将模型和属性作为输入，并输出属性为真或反驳属性的反例。”[50]。在这项研究中，我们更青睐可达性分析而不是其他方法，比如图匹配方法，因为它提供了机会来深入和自动地检查所有可能的路径，以检查安全属性的满足情况，同时在计算上比图匹配更经济。0对于所示的组合线性时间安全属性集0图5中，我们使用Uppaal进行可达性分析，以查看哪些属性得到满足，哪些没有。这一过程的结果使我们能够检查Tom的行为，并确定他的安全弱点。我们通过Uppaal的两个可达性分析结果示例，确定Tom启用了手动更新，并且没有在新版本发布的第一天内安装新的更新。0Uppaal执行可达性分析，并检查状态是否0使用广度优先搜索（BFS）或深度优先搜索（DFS）算法来遍历图形。我们选择广度优先搜索（BFS）来检查我们的可达性属性（即安全属性）在用户状态转换图中的满意度，因为它可以轻松地遍历图形。06.3. 策略生成0实验执行后，我们能够检查0
