本文将概述几篇云上形式化验证的论文，其中大部分源于 amazon.science 里的 Automated Reasoning 分类。
本文关注的重点方向包括：
英语术语
中文术语
含义
Policy 策略
用于形式化表达一组 IAM 授权，是由 Statement 构成的一个数组
Statement 语句
构成策略数组的元素，包含 Effect , Action , Conditon , Resource 等维度
Effect 效果
Allow 和 Deny 二选一，表示本条 Statement 是授权语义和拒绝语义
Action 权限
表示本条 Statement 关联的授权或拒绝的权限点
Resource 资源
表示本条 Statement 关联的授权或拒绝的资源
Condition 条件
表示本条 Statement 关联的授权或拒绝的条件；AWS 提供丰富了的条件键
Match 命中/匹配
表示一组请求是否同时满足本条 Statement 的 Action , Resource 和 Condition
AWS 策略的总体规则：当一组真实请求命中至少一条 Allow 语句且没有命中任何 Deny 语句则鉴权通过。
会议或期刊名
CCF 评级
C omputer A ided V erificationA
Conference on O bject-O riented P rogramming S ystems, L anguages, and A pplications
A
Usenix Security SymposiumA
Theory and Applications of Sat isfiability Testing
B
F ormal M ethods in C omputer-A ided DesignC
IP Counting in Public Access
FMCAD 2024, AWS, Loris D’Antoni: Projective model counting for IP addresses in access control policies
简介 ：Zelkova 想根据“授权的 IP 数量是否超过特定阈值”来判断策略是否是 Public Access。论文基于 bounded projective IP-counting problem 提出了两种编码方式，使得 99.999% 的策略都能在 3s 内出解。
IP 等价类 ：一个很自然的想法。由于策略里每条针对 IP 的 Condition 一定是 CIDR 格式，且真实场景里用户策略不会太长，可以借助离散化的思想，把 2 32 2^{32} 2 32
基础编码方式 ：设 IP 的等价类是 S 1 , S 2 , … , S n S_1,S_2,\dots,S_n S 1 , S 2 , … , S n ∣ S i ∣ |S_i| ∣ S i ∣ s i s_i s i S i S_i S i s i ∈ S i s_i \in S_i s i ∈ S i φ p ( x , i p ) \varphi_p(\mathbf{x},ip) φ p ( x , i p ) p p p S i S_i S i φ p ( x , i p = s i ) \varphi_p(\mathbf{x},ip=s_i) φ p ( x , i p = s i ) ∣ S i ∣ |S_i| ∣ S i ∣
方式一：Arithmetic Approach 。论文认为同时支持 arithmetic 和 string 理论的 SMT 求解器（如 CVC5, Z3 等主流求解器）经过如下一次编码和求解即可完成阈值判断。我认为这 n n n φ p ( x ) \varphi_p(\mathbf{x}) φ p ( x )
( ∑ i = 1 n { ∣ S i ∣ if ∃ x . φ p ( x , i p ) 0 otherwise ) ≥ thresold \left(\sum_{i=1}^n
\begin{cases}
|S_i| \quad &\text{if }~\exists \mathbf{x}.~\varphi_p(\mathbf{x},ip) \\
0 &\text{otherwise}
\end{cases}\right) \ge \text{thresold}
( i = 1 ∑ n { ∣ S i ∣ 0 if ∃ x . φ p ( x , i p ) otherwise ) ≥ thresold
方式二：Arithmetic-free Approach 。对于不支持 arithmetic 的求解器（如 AWS 自研的 NFA2SAT ），论文先用背包找到所有 IP 等价类的极小集 { T 1 , T 2 , … , T m } \{T_1,T_2,\dots,T_m\} { T 1 , T 2 , … , T m } ∀ i ≠ j T i ⊈ T j \forall_{i\ne j} T_i \not \subseteq T_j ∀ i = j T i ⊆ T j ∀ i ( ∑ S j ∈ T i ∣ S j ∣ ) ≥ thresold \forall_i (\sum _{S_j \in T_i} |S_j|) \ge \text{thresold} ∀ i ( ∑ S j ∈ T i ∣ S j ∣ ) ≥ thresold
SMT-D
FMCAD 2024, AWS, Clark Barrett: SMT-D: New Strategies for Portfolio-Based SMT Solving :
简介
论文提出了名为 SMT-D 的基于 CVC5 实例的 Portfolio 框架，主打基于 Clause Sharing 的规则分享机制，叠加上 Delayed Sharing 和 Guided Randomization 两种特性，总体效果好于基于 OPENSMT2 实例的 SMTS。
SMTS 同时支持 Clause Sharing 和 Partition 机制，本论文做 SMTS 实验时没有开启 Partition 的开关。
CVC5-P 仅支持 Partition 机制，本论文做 CVC5-P 实验时默认保持了这一机制。
从第二张图单实例对比中可以看出 OPENSMT2 好于 CVC5，但加了 64 节点的分享后 SMT-D 超过了 SMTS。
术语
解释
Delayed Sharing 强制要求每个求解器在 preprocessing 阶段后才能分享 lemma
Guided Randomization 观察到随着集群规模的增大，配置各异的求解器能唯一学到的规则数量趋于饱和。将集群分成 normal 和 noisy 两块，后者拥有更激进的参数配置且只导入导出更短的 lemma 。
CS / CS-GR
仅带有 Clause Sharing / 同时带有 Clause Sharing 和 Guided Randomization
PAR-2
SAT 竞赛的计分方式，统计所有实例的用时之和，超时（ > 1200 s >1200s > 1200 s
SMT-D
当前混合求解器框架的 SOTA（SMT COMP 22 Cloud Track）
框架
论文抽象了中心化的 Controller 负责信息交换和监控，底下每个 Worker 能互相分享学到的新规则（lemma ）。
Controller 用 python 实现 ，gRPC 通信（便于跨场景），交互格式选用宽松但是直观的 SMTLIB。
Controller 用 “上一次发送至今的间隔” 和 “待发送的 lemma 队列长度” 两个维度来决定 shouldSend 函数。实测发现即收即发的效果不错，因为使用的 CVC5 每秒钟支持导入超过 1000 1000 1000 lemma ，即使是 64 实例的求解器集群，在 ∣ l e m m a ∣ ≤ 8 |lemma| \le 8 ∣ l e mma ∣ ≤ 8 1 / 214 1/214 1/214
用 lemma 里的子句数量来衡量价值。每个求解器不会分享包含新变量的 lemma 。
normal 集群和 noisy 集群数量各占 ( 75 % , 25 % ) (75\%,25\%) ( 75% , 25% ) rnd_freq 参数，前者默认后者开到 75 % 75\% 75% ≤ 8 \le 8 ≤ 8 = 1 =1 = 1 ≤ 4 \le 4 ≤ 4
NFA2SAT with Concatenation
FMCAD 2024, AWS, Kevin Lotz: Solving String Constraints with Concatenation Using SAT
Reduce Privilege for Policy
OOPSLA 2024, AWS, Loris D’Antoni: Automatically reducing privilege for access control policies
简介
本文专注于 AWS 策略生成场景，即给出原始策略和一些已通过的请求集合，IAM-PolicyRefiner 会生成一个满足最小化权限的新策略 。本论文提出了三个评价维度，最大的特色是将 Readability 这个感性的维度给量化。
维度
粗略解释
Readability 策略的可读性，即让新策略在字面量尽可能的和原来保持接近。
Soundness 策略的合理性，即能让已通过的请求仍然保持正确授权。
Tightness 策略的紧密性，即满足前两个条件下授权语义越小越好。
IAM-PolicyRefiner 的整体流程是：读取 AWS Cloud Trail 里所有鉴权通过的请求，找到每个请求对应的授权策略里第一条匹配的语句，计算该语句 s s s S s \mathcal{S}_s S s Readability 的策略集。整个 IAM-PolicyRefiner 用 ∼ 3000 \sim 3000 ∼ 3000
Abstraction 和 Well-Behaved 的定义
为了方便阐述论文的推理细节，本文约定以下记号：
符号
概念
M ( s ) M(s) M ( s ) 语句 s s s
e e e 表示一条语句的效果是 Allow 还是 Deny
Ψ : V → pred \Psi:V \to \text{pred} Ψ : V → pred 表示一条语句的具体约束，将所有变量映射成断言
C C C 待匹配的请求（Request）的总集
A A A 所有尝试去匹配这些请求的策略全集
Σ , σ , Σ ∗ \Sigma,\sigma,\Sigma^* Σ , σ , Σ ∗ 单个字符的集合，不含通配符的字符串，不含通配符的字符串总集
p a t , L ( p a t ) pat,\mathcal{L}(pat) p a t , L ( p a t ) 正则约束，正则约束匹配的所有不含通配符的字符串集合
Ω ( σ , p a t ) \Omega(\sigma,pat) Ω ( σ , p a t ) σ \sigma σ p a t pat p a t
下面在策略集合 A A A ⊑ \sqsubseteq ⊑
符号
概念
( A , ⊑ ) (A,\sqsubseteq) ( A , ⊑ ) a ⊑ b , ( a , b ) ∈ A a \sqsubseteq b,(a,b) \in A a ⊑ b , ( a , b ) ∈ A a a a b b b
( A , ⊔ ) (A, \sqcup) ( A , ⊔ ) m = a ⊔ b , ( a , b , m ) ∈ A m=a \sqcup b,(a,b,m) \in A m = a ⊔ b , ( a , b , m ) ∈ A a a a b b b A A A a ⊑ w , b ⊑ w a \sqsubseteq w, b \sqsubseteq w a ⊑ w , b ⊑ w ∀ w ∈ A , a ⊑ w ∧ b ⊑ w → m ⊑ w \forall w \in A, a \sqsubseteq w \land b \sqsubseteq w \to m \sqsubseteq w ∀ w ∈ A , a ⊑ w ∧ b ⊑ w → m ⊑ w
⊥ \bot ⊥ A A A ⊑ \sqsubseteq ⊑ ∀ a ∈ A , ⊥ ⊑ A \forall a \in A, \bot \sqsubseteq A ∀ a ∈ A , ⊥ ⊑ A
γ ( A ↦ 2 C ) \gamma(A \mapsto 2^C) γ ( A ↦ 2 C ) 将一条策略 a a a
β ( C ↦ A ) \beta(C \mapsto A) β ( C ↦ A ) 能匹配某一条请求 c c c ⊑ \sqsubseteq ⊑ a a a
将一组满足上述全部性质的 Abstraction A = ( C , A , ⊑ , β , γ , ⊔ , ⊥ ) \mathcal{A}=(C,A,\sqsubseteq,\beta,\gamma,\sqcup,\bot) A = ( C , A , ⊑ , β , γ , ⊔ , ⊥ ) Well-behaved 。此时 ∀ D ⊆ C \forall D \subseteq C ∀ D ⊆ C a ∈ A a \in A a ∈ A D ⊆ γ ( a ) D \subseteq \gamma(a) D ⊆ γ ( a ) ∀ b ∈ A , D ⊆ γ ( b ) b ⊆ a \forall_{b \in A,D \subseteq \gamma(b) } b \subseteq a ∀ b ∈ A , D ⊆ γ ( b ) b ⊆ a a a a
a = ⨆ d ∈ D β ( d ) a=\bigsqcup_{d \in D}\beta(d)
a = d ∈ D ⨆ β ( d )
策略的搜索空间和 Abstraction 构造
Predicate Search Space Φ ψ [ v ] \Phi_{\psi[v]} Φ ψ [ v ] v v v Ψ [ v ] \Psi[v] Ψ [ v ]
Statement Search Space S s \mathcal{S}_s S s ：相比原始语句 s = ( e , Ψ ) s=(e,\Psi) s = ( e , Ψ ) Predicate Search Space 里取值。
( e , Ψ ′ ) ∈ S s ⟺ V ( Ψ s ) = V ( Ψ ′ ) ⋀ ∀ v ∈ V ( Ψ ) Ψ ′ [ v ] ∈ Φ Ψ [ v ] (e,\Psi') \in \mathcal{S}_s \iff V(\Psi_s)=V(\Psi') \bigwedge \forall_{v \in V(\Psi)} \Psi'[v] \in \Phi_{\Psi[v]}
( e , Ψ ′ ) ∈ S s ⟺ V ( Ψ s ) = V ( Ψ ′ ) ⋀ ∀ v ∈ V ( Ψ ) Ψ ′ [ v ] ∈ Φ Ψ [ v ]
Policy Search Space P p \mathcal{P}_p P p Statement Search Space 里取值。
若语句 s = ( e , Ψ ) s=(e,\Psi) s = ( e , Ψ ) ψ ∈ p r e d ( s ) \psi \in pred(s) ψ ∈ p re d ( s ) A ψ = ( v a l ( ψ ) , Φ ψ , → , β ψ , γ ψ , ⊔ ψ , ⊥ ) \mathcal{A_\psi}=(val(\psi),\Phi_\psi,\to,\beta_{\psi},\gamma_{\psi},\sqcup_{\psi},\bot) A ψ = ( v a l ( ψ ) , Φ ψ , → , β ψ , γ ψ , ⊔ ψ , ⊥ ) Well-behaved 的，则针对 S s \mathcal{S}_s S s Abstraction A s = ( M ( s ) , S s , ⊑ s , β s , γ s , ⊔ s , ⊥ ) \mathcal{A}_{\mathcal{s}}=(M(s), \mathcal{S}_s,\sqsubseteq_{\mathcal{s}},\beta_{\mathcal{s}},\gamma_{\mathcal{s}},\sqcup_{\mathcal{s}},\bot) A s = ( M ( s ) , S s , ⊑ s , β s , γ s , ⊔ s , ⊥ ) Well-behaved 的：
a ⊑ s b ⟺ { M ( a ) ⊆ M ( b ) if e = a l l o w M ( b ) ⊆ M ( a ) if e = d e n y β s ( r ) = ( e , Ψ ′ ) ∈ S s s.t. V ( Ψ ) = V ( Ψ ′ ) ∧ ∀ v ∈ V ( Ψ ) Ψ ′ [ v ] = β Ψ [ v ] ( r ( v ) ) γ s ( e , Ψ ′ ) = M ( Ψ ′ ) ( e , Ψ 1 ) ⊔ s ( e , Ψ 2 ) = ( e , Ψ ′ ) s.t. ∀ v ∈ V ( Ψ ) Ψ ′ [ v ] = Ψ 1 [ v ] ⊔ Ψ [ v ] Ψ 2 [ v ] \begin{aligned}
a \sqsubseteq_{\mathcal{s}}& b \iff \begin{cases}
M(a) \subseteq M(b) & \text{if } e=allow \\
M(b) \subseteq M(a) & \text{if } e=deny \\
\end{cases} \\
\beta_{\mathcal{s}}(r)&=(e,\Psi') \in \mathcal{S}_s \quad \text{s.t.} \quad V(\Psi)=V(\Psi') ~\land~ \forall_{v \in V(\Psi)} \Psi'[v]=\beta_{\Psi[v]}(r(v)) \\
\gamma_{\mathcal{s}}(e,\Psi')&=M(\Psi') \\
(e,\Psi_1) \sqcup_{\mathcal{s}}(e,\Psi_2)&=(e,\Psi')\quad \text{s.t.} \quad \forall_{v \in V(\Psi)} \Psi'[v]=\Psi_1[v] \sqcup_{\Psi[v]}\Psi_2[v] \\
\end{aligned}
a ⊑ s β s ( r ) γ s ( e , Ψ ′ ) ( e , Ψ 1 ) ⊔ s ( e , Ψ 2 ) b ⟺ { M ( a ) ⊆ M ( b ) M ( b ) ⊆ M ( a ) if e = a ll o w if e = d e n y = ( e , Ψ ′ ) ∈ S s s.t. V ( Ψ ) = V ( Ψ ′ ) ∧ ∀ v ∈ V ( Ψ ) Ψ ′ [ v ] = β Ψ [ v ] ( r ( v )) = M ( Ψ ′ ) = ( e , Ψ ′ ) s.t. ∀ v ∈ V ( Ψ ) Ψ ′ [ v ] = Ψ 1 [ v ] ⊔ Ψ [ v ] Ψ 2 [ v ]
若策略 p = ( A l l o w : { a 1 , a 2 , … , a n } , D e n y : { d 1 , d 2 , … , d m } ) p=(Allow:\{a_1,a_2,\dots,a_n\},Deny:\{d_1,d_2,\dots,d_m\}) p = ( A ll o w : { a 1 , a 2 , … , a n } , De n y : { d 1 , d 2 , … , d m }) ψ ∈ ⋃ i p r e d ( a i ) \psi \in \bigcup_i pred(a_i) ψ ∈ ⋃ i p re d ( a i ) A ψ \mathcal{A_\psi} A ψ Well-behaved 的，现在针对 P p \mathcal{P}_p P p Abstraction A P = ( G r a n t e d ( p ) , P p , ⊑ P , β P , γ P , ⊔ P , ⊥ ) \mathcal{A}_{\mathcal{P}}=(Granted(p), \mathcal{P}_p,\sqsubseteq_{\mathcal{P}},\beta_{\mathcal{P}},\gamma_{\mathcal{P}},\sqcup_{\mathcal{P}},\bot) A P = ( G r an t e d ( p ) , P p , ⊑ P , β P , γ P , ⊔ P , ⊥ )
a ⊑ P b ⟺ G r a n t e d ( a ) ⊆ G r a n t e d ( b ) β P ( r ) = { a 1 ′ , … , a n ′ , d 1 , … , d m } s.t. ∀ 1 ≤ i ≤ n { a i ′ = ⊥ r ∈ ∪ j < i M ( a j ) ∨ r ∉ M ( a i ) a i ′ = β a i ( r ) otherwise γ P ( P ′ ) = G r a n t e d ( P ′ ) { a 1 1 , … , a n 1 , d 1 , … , d m } ⊔ P { a 1 2 , … , a n 2 , d 1 , … , d m } = { a 1 1 ⊔ a 1 a 1 2 , … , a n 1 ⊔ a n a n 2 , d 1 , … , d m } \begin{aligned}
a \sqsubseteq_{\mathcal{P}}& b \iff Granted(a) \subseteq Granted(b) \\
\beta_{\mathcal{P}}(r)&=\{a_1',\dots,a_n',d_1,\dots,d_m\} \text{ s.t. } \forall_{1 \le i \le n} \begin{cases}
a_i'=\bot & r \in \cup_{j<i}M(a_j) \lor r \notin M(a_i) \\
a_i'=\beta_{a_i}(r) & \text{otherwise} \\
\end{cases} \\
\gamma_{\mathcal{P}}(P')&=Granted(P') \\
\{a_1^1,\dots,a_n^1,d_1,\dots,d_m\} &\sqcup_{\mathcal{P}} \{a_1^2,\dots,a_n^2,d_1,\dots, d_m\}=\{a_1^1 \sqcup_{a_1}a_1^2,\dots,a_n^1 \sqcup_{a_n}a_n^2,d_1,\dots,d_m\}
\end{aligned}
a ⊑ P β P ( r ) γ P ( P ′ ) { a 1 1 , … , a n 1 , d 1 , … , d m } b ⟺ G r an t e d ( a ) ⊆ G r an t e d ( b ) = { a 1 ′ , … , a n ′ , d 1 , … , d m } s.t. ∀ 1 ≤ i ≤ n { a i ′ = ⊥ a i ′ = β a i ( r ) r ∈ ∪ j < i M ( a j ) ∨ r ∈ / M ( a i ) otherwise = G r an t e d ( P ′ ) ⊔ P { a 1 2 , … , a n 2 , d 1 , … , d m } = { a 1 1 ⊔ a 1 a 1 2 , … , a n 1 ⊔ a n a n 2 , d 1 , … , d m }
注意 A P \mathcal{A_{\mathcal{P}}} A P 不是 Well-behaved 的，反例如下：p p p a ∗ a* a ∗ ∗ b *b ∗ b r r r a b ab ab P p \mathcal{P}_p P p β ( r ) \beta(r) β ( r ) a b ∗ ab* ab ∗ ⊥ \bot ⊥ ⊥ \bot ⊥ ∗ a b *ab ∗ ab
若 p p p ∀ 1 ≤ i < j ≤ n M ( a i ) ∩ M ( a j ) = ∅ \forall_{1 \le i < j \le n} M(a_i) \cap M(a_j)=\emptyset ∀ 1 ≤ i < j ≤ n M ( a i ) ∩ M ( a j ) = ∅ A P A_{\mathcal{P}} A P 是 Well-behaved 。
不同类型的 Abstraction 构造
相等构造 ：对于 v = c v=c v = c C = { c } C=\{c\} C = { c } A = { v = c , ⊥ } A=\{v=c,\bot\} A = { v = c , ⊥ } Well-behaved 的。
不等构造 ：对于 v ≠ c v \ne c v = c Well-behaved 的 A ≠ c = ( v a l ( ≠ c ) , Φ ≠ c , → , β ≠ c , γ ≠ c , ⊔ ≠ c , ⊥ ) \mathcal{A}_{\ne c}=(val(\ne c), \Phi_{\ne c},\to,\beta_{\ne c},\gamma_{\ne c},\sqcup_{\ne c},\bot) A = c = ( v a l ( = c ) , Φ = c , → , β = c , γ = c , ⊔ = c , ⊥ )
v a l ( ≠ c ) = { d ∣ d ≠ c ∧ d ∈ V a l u e s t y p e ( c ) ( p ) } , i.e. all values ≠ d and has same type as c Φ ≠ c = { v = d ∣ d ≠ c } ∪ { v ≠ c } ∪ { ⊥ } β ≠ c = v = d γ ≠ c ( v = d ) = { d } , γ ≠ c ( v ≠ c ) = v a l ( ≠ c ) a ⊔ ≠ c b = { a b → a b a → b v ≠ c otherwise \begin{aligned}
val(\ne c)&=\{d | d \ne c \land d \in Values_{type(c)}(p)\}, \text{i.e. all values } \ne d\text{ and has same type as }c \\
\Phi_{\ne c}&=\{v=d | d \ne c\} \cup \{v \ne c\} \cup \{\bot\} \\
\beta_{\ne c}&= \quad v=d \\
\gamma_{\ne c}(v=d)&=\{d\},\gamma_{\ne c}(v \ne c)=val(\ne c) \\
a \sqcup_{\ne c} b&=\begin{cases}
a& b \to a \\
b& a \to b \\
v \ne c & \text{otherwise}
\end{cases}
\end{aligned}
v a l ( = c ) Φ = c β = c γ = c ( v = d ) a ⊔ = c b = { d ∣ d = c ∧ d ∈ Va l u e s t y p e ( c ) ( p )} , i.e. all values = d and has same type as c = { v = d ∣ d = c } ∪ { v = c } ∪ { ⊥ } = v = d = { d } , γ = c ( v = c ) = v a l ( = c ) = ⎩ ⎨ ⎧ a b v = c b → a a → b otherwise
比较构造 ：对于 v ≤ c v \le c v ≤ c C = { d ∣ d ≤ c ∧ d ∈ V a l u e s t y p e ( c ) ( p ) } C=\{d | d \le c \land d \in Values_{type(c)}(p)\} C = { d ∣ d ≤ c ∧ d ∈ Va l u e s t y p e ( c ) ( p )} Well-behaved 的。
通配符 ? 构造 ：考虑 C = Σ C=\Sigma C = Σ A = Σ ∪ { ? } ∪ { ⊥ } A=\Sigma \cup \{?\} \cup \{\bot \} A = Σ ∪ { ?} ∪ { ⊥ } Well-behaved 的。
通配符 * 构造 ：包含 * 和 σ \sigma σ A ∗ \mathcal{A}_{*} A ∗ Well-behaved 的是 A p r e f \mathcal{A}_{pref} A p re f A s u c c \mathcal{A}_{succ} A s u cc
字符串前缀构造 ：构造如下的 Well-behaved 的 A p r e f = ( Σ ∗ , Φ p r e f , ⊆ L , β p r e f , γ p r e f , ⊔ p r e f , ⊥ ) \mathcal{A}_{pref}=(\Sigma^*, \Phi_{pref},\subseteq_{\mathcal{L}},\beta_{pref},\gamma_{pref},\sqcup_{pref},\bot) A p re f = ( Σ ∗ , Φ p re f , ⊆ L , β p re f , γ p re f , ⊔ p re f , ⊥ )
Φ p r e f = Σ ∗ ∪ { σ W ∣ σ ∈ Σ ∗ ∧ W ∈ { ? , ∗ } } ∪ { ⊥ } β p r e f ( σ ) = σ γ ( p a t ) = L ( p a t ) x ⊔ p r e f y = { x y → x y x → y z ? z = l c p ( x , y ) ∧ ∣ z ∣ + 1 = ∣ x ∣ = ∣ y ∣ ∧ x ≠ z ? ∧ y ≠ z ? z ∗ z = l c p ( x , y ) \begin{aligned}
\Phi_{pref} &= \Sigma^* \cup \left\{\sigma W | \sigma \in \Sigma^* \land W \in \{?,*\} \right\} \cup \{\bot\} \\
\beta_{pref}(\sigma)&=\sigma \\
\gamma(pat)&=\mathcal{L}(pat) \\
x \sqcup_{pref} y&=\begin{cases}
x & y \to x \\
y & x \to y \\
z? & z=lcp(x,y) \land |z|+1=|x|=|y| \land x \ne z? \land y \ne z? \\
z* & z=lcp(x,y)
\end{cases}
\end{aligned}
Φ p re f β p re f ( σ ) γ ( p a t ) x ⊔ p re f y = Σ ∗ ∪ { σW ∣ σ ∈ Σ ∗ ∧ W ∈ { ? , ∗ } } ∪ { ⊥ } = σ = L ( p a t ) = ⎩ ⎨ ⎧ x y z ? z ∗ y → x x → y z = l c p ( x , y ) ∧ ∣ z ∣ + 1 = ∣ x ∣ = ∣ y ∣ ∧ x = z ? ∧ y = z ? z = l c p ( x , y )
字符串前后缀构造 ：一个很自然的想法是将 A p r e f \mathcal{A}_{pref} A p re f A s u c c \mathcal{A}_{succ} A s u cc A p r e f + s u f f \mathcal{A}_{pref+suff} A p re f + s u ff { a a , a a a , a c a } \{aa,aaa,aca\} { aa , aaa , a c a } ( a ∗ , ∗ a ) (a*,*a) ( a ∗ , ∗ a ) a ∗ a a*a a ∗ a { a a , a a a } \{aa,aaa\} { aa , aaa } ( a a ∗ , ∗ a a ) (aa*,*aa) ( aa ∗ , ∗ aa ) a a ∗ a a aa*aa aa ∗ aa 4 4 4 A p r e f + s u f f \mathcal{A}_{pref+suff} A p re f + s u ff ∣ p p r e f ∣ + ∣ p s u c c ∣ |p_{pref}|+|p_{succ}| ∣ p p re f ∣ + ∣ p s u cc ∣ Soundness 的，可以用来替代 A ∗ \mathcal{A}_{*} A ∗
特定正则串构造 ：对于特定的正则串 p a t = σ 0 W 1 σ 1 … W n σ n pat=\sigma_0W_1\sigma_1\dots W_n\sigma_n p a t = σ 0 W 1 σ 1 … W n σ n W i ∈ { ∗ , ? } W_i \in \{*,?\} W i ∈ { ∗ , ?} A ∗ \mathcal{A}_* A ∗ A ? \mathcal{A}_? A ? A p a t = ( L ( p a t ) , Φ p a t , ⊆ L , β p a t , γ p a t , ⊔ p a t , ⊥ ) \mathcal{A}_{pat}=(\mathcal{L}(pat),\Phi_{pat}, \subseteq_{\mathcal{L}}, \beta_{pat},\gamma_{pat},\sqcup_{pat},\bot) A p a t = ( L ( p a t ) , Φ p a t , ⊆ L , β p a t , γ p a t , ⊔ p a t , ⊥ )
Φ p a t = { σ 0 x 1 σ 1 … x n σ n ∣ x i ∈ Φ W i } ∪ { ⊥ } β p a t ( σ ) = σ 0 x 1 σ 1 … x n σ n s.t. x i = Ω ( σ , p a t ) [ 0 ] [ i ] γ p a t ( p a t ′ ) = L ( p a t ′ ) p a t 1 ⊔ p a t p a t 2 = { p a t 1 p a t 2 → p a t 1 p a t 2 p a t 1 → p a t 2 σ 0 z 1 σ 1 … z n σ n s.t. ∀ i z i = x i 1 ⊔ W i x i 2 otherwise \begin{aligned}
\Phi_{pat}&=\{\sigma_0x_1\sigma_1\dots x_n\sigma_n\ | x_i \in \Phi_{W_i}\} \cup \{\bot\} \\
\beta_{pat}(\sigma)&=\sigma_0x_1\sigma_1\dots x_n\sigma_n \quad \text{s.t. }x_i=\Omega(\sigma,pat)[0][i] \\
\gamma_{pat}(pat')&=\mathcal{L}(pat') \\
pat_1 \sqcup_{pat} pat_2 &= \begin{cases}
pat_1 & pat_2 \to pat_1 \\
pat_2 & pat_1 \to pat_2 \\
\sigma_0z_1\sigma_1\dots z_n\sigma_n \quad \text{s.t. } \forall_i z_i=x_i^1 \sqcup_{W_i}x_i^2 & \text{otherwise}
\end{cases}
\end{aligned}
Φ p a t β p a t ( σ ) γ p a t ( p a t ′ ) p a t 1 ⊔ p a t p a t 2 = { σ 0 x 1 σ 1 … x n σ n ∣ x i ∈ Φ W i } ∪ { ⊥ } = σ 0 x 1 σ 1 … x n σ n s.t. x i = Ω ( σ , p a t ) [ 0 ] [ i ] = L ( p a t ′ ) = ⎩ ⎨ ⎧ p a t 1 p a t 2 σ 0 z 1 σ 1 … z n σ n s.t. ∀ i z i = x i 1 ⊔ W i x i 2 p a t 2 → p a t 1 p a t 1 → p a t 2 otherwise
可惜 A p a t \mathcal{A}_{pat} A p a t 不是 Well-behaved 的，因为 β ( σ ) \beta(\sigma) β ( σ ) p a t = a ∗ a ∗ pat=a*a* p a t = a ∗ a ∗
σ \sigma σ Ω ( σ i , p a t ) \Omega(\sigma_i,pat) Ω ( σ i , p a t )
σ 1 = a a a a \sigma_1=aaaa σ 1 = aaaa [ ( a a , ϵ ) , ( a , a ) , ( ϵ , a a ) ] [(aa,\epsilon),(a,a),(\epsilon,aa)] [( aa , ϵ ) , ( a , a ) , ( ϵ , aa )]
σ 2 = a a a a a \sigma_2=aaaaa σ 2 = aaaaa [ ( a a a , ϵ ) , ( a a , a ) , ( a , a a ) , ( ϵ , a a a ) ] [(aaa,\epsilon),(aa,a),(a,aa),(\epsilon,aaa)] [( aaa , ϵ ) , ( aa , a ) , ( a , aa ) , ( ϵ , aaa )]
σ 3 = a b a a \sigma_3=abaa σ 3 = abaa [ ( b , a ) ] [(b,a)] [( b , a )]
β ( σ i ) \beta(\sigma_i) β ( σ i ) { a a , a a a , b } \{aa,aaa,b\} { aa , aaa , b } { ϵ , ϵ , a } \{\epsilon,\epsilon,a\} { ϵ , ϵ , a } ( ∗ , ∗ ) (*,*) ( ∗ , ∗ ) { a , a , b } \{a,a,b\} { a , a , b } { a , a a , a } \{a,aa,a\} { a , aa , a } ( ? , a ∗ ) (?,a*) ( ? , a ∗ )
论文把 ∃ σ , ∣ Ω ( σ , p a t ) ∣ > 1 \exist \sigma,|\Omega(\sigma,pat)|>1 ∃ σ , ∣Ω ( σ , p a t ) ∣ > 1 p a t pat p a t ambiguous pattern ，指出 unambiguous 的 A p a t \mathcal{A}_{pat} A p a t 是 Well-behaved 的。
析取构造 ：ψ ∨ = ψ 1 ∨ ⋯ ∨ ψ n \psi_{\lor}=\psi_1 \lor \dots \lor \psi_n ψ ∨ = ψ 1 ∨ ⋯ ∨ ψ n Well-behaved 的，如果 ∀ i A ψ i \forall_i \mathcal{A}_{\psi_i} ∀ i A ψ i Well-behaved 的。
合取构造 ：ψ ∧ = ψ 1 ∧ ⋯ ∧ ψ n \psi_{\land}=\psi_1 \land \dots \land \psi_n ψ ∧ = ψ 1 ∧ ⋯ ∧ ψ n Well-behaved 的，如果 ∀ i A ψ i \forall_i \mathcal{A}_{\psi_i} ∀ i A ψ i Well-behaved 的。
IAM-PolicyRefinerNeg
从请求集 C C C C C C P p \mathcal{P}_p P p
NFA2SAT
CAV 2023, AWS, Kevin Lotz: Solving String Constraints Using SAT
简介
提出了 NFA2SAT 的字符串约束求解器，使用 CaDiCaL 作为后端，将字符串约束转化为纯 SAT 约束迭代式求解。整体思想类似 WOORPJE，但证明了迭代长度的上限，可以在有限步停止并输出 UNSAT。
对比经典的 SMT 求解器，NFA2DFA 更适合 SAT 但不适合 UNSAT。ZALIGVINDER 测试集上结果如下：
框架
本文考虑的字符串命题 ψ \psi ψ
F = F ∨ F ∣ F ∧ F ∣ ¬ F ∣ Atom A t o m = x ∈ R E ∣ x = y R E = R E ∪ R E ∣ R E ⋅ R E ∣ R E ∗ ∣ R E ∩ R E ∣ ? ∣ w \begin{align}
F&=F \lor F \mid F \land F \mid \lnot F \mid \text{Atom} \\
Atom&=x \in RE \mid x=y \\
RE&=RE \cup RE \mid RE \cdot RE \mid RE^* \mid RE \cap RE \mid ? \mid w
\end{align}
F A t o m RE = F ∨ F ∣ F ∧ F ∣ ¬ F ∣ Atom = x ∈ RE ∣ x = y = RE ∪ RE ∣ RE ⋅ RE ∣ R E ∗ ∣ RE ∩ RE ∣ ? ∣ w
利用 BMC 思想，将字符串命题 ψ \psi ψ b b b ψ A ∧ D b ∧ h b \psi_{\mathcal{A}} \land \mathbf{D}^b \land h^b ψ A ∧ D b ∧ h b
ψ A \psi_{\mathcal{A}} ψ A x ∈ R E , x = y x \in RE,x=y x ∈ RE , x = y D b ∧ h b \mathbf{D}^b \land h^b D b ∧ h b b b b
字母表缩减技术
论文证明了字符串命题 ψ \psi ψ
增量编码细节
字符串变量 x x x ：假设第 k k k b k ( x ) b_k(x) b k ( x ) b k ( x ) × ( ∣ Σ ∣ + 1 ) b_k(x) \times (|\Sigma|+1) b k ( x ) × ( ∣Σ∣ + 1 ) x [ i ] x[i] x [ i ] j j j λ \lambda λ Σ \Sigma Σ
h b k − 1 b k = ( ⋀ x ⋀ b k − 1 ( x ) + 1 b k ( x ) E x a c t O n e ( h x [ i ] a ∣ a ∈ { Σ , λ } ) ) ∧ ( ⋀ x ⋀ b k − 1 ( x ) b k ( x ) − 1 h x [ i ] λ → h x [ i + 1 ] λ ) h^{b_{k}}_{b_{k-1}}=\left(\bigwedge_{x} \bigwedge_{b_{k-1}(x)+1}^{b_{k}(x)} ExactOne({h^a_{x[i]}} | a \in \{\Sigma, \lambda\})\right) \land \left(\bigwedge_{x} \bigwedge_{b_{k-1}(x)}^{b_{k}(x)-1} h_{x[i]}^\lambda \to h_{x[i+1]}^\lambda \right)
h b k − 1 b k = ⎝ ⎛ x ⋀ b k − 1 ( x ) + 1 ⋀ b k ( x ) E x a c tO n e ( h x [ i ] a ∣ a ∈ { Σ , λ }) ⎠ ⎞ ∧ ⎝ ⎛ x ⋀ b k − 1 ( x ) ⋀ b k ( x ) − 1 h x [ i ] λ → h x [ i + 1 ] λ ⎠ ⎞
其中第二部分是用来限制占位符后必须全是占位符，保证解的唯一性。
正则约束 x ∈ R x \in R x ∈ R ：构造对应的 NFA ( Q , Σ , δ , q 0 , F ) (Q,\Sigma,\delta,q_0,F) ( Q , Σ , δ , q 0 , F ) q q q λ \lambda λ S q i S_q^i S q i x [ 1.. i ] x[1..i] x [ 1.. i ] q q q
通过枚举状态和转移边的组合 ( q , a ) → q ′ (q,a) \to q' ( q , a ) → q ′
⋀ b k − 1 ( x ) b k ( x ) − 1 ⋀ ( q , a ) ∈ d o m ( δ ) ⋀ q ′ ∈ δ ( q , a ) ( S q i ∧ h x [ i + 1 ] a ) → S q ′ i + 1 \bigwedge_{b_{k-1}(x)}^{b_{k}(x)-1} \bigwedge_{(q,a) \in dom(\delta)} \bigwedge_{q' \in \delta(q,a)} (S_q^i \land h_{x[i+1]}^a) \to S_{q'}^{i+1}
b k − 1 ( x ) ⋀ b k ( x ) − 1 ( q , a ) ∈ d o m ( δ ) ⋀ q ′ ∈ δ ( q , a ) ⋀ ( S q i ∧ h x [ i + 1 ] a ) → S q ′ i + 1
每个 S q i S_q^i S q i S q ′ i S_{q'}^i S q ′ i S q i − 1 S_q^{i-1} S q i − 1
⋀ b k − 1 ( x ) + 1 b k ( x ) ⋀ q ′ ∈ Q ( S q ′ i → ⋁ ( q , a ) ∈ p r e d ( q ′ ) ( S q i − 1 ∧ h x [ i ] a ) ) \bigwedge_{b_{k-1}(x)+1}^{b_{k}(x)} \bigwedge_{q'\in Q} \left(S_{q'}^i \to \bigvee_{(q,a) \in pred(q')} (S_q^{i-1} \land h_{x[i]}^a)\right)
b k − 1 ( x ) + 1 ⋀ b k ( x ) q ′ ∈ Q ⋀ ⎝ ⎛ S q ′ i → ( q , a ) ∈ p re d ( q ′ ) ⋁ ( S q i − 1 ∧ h x [ i ] a ) ⎠ ⎞
第 k k k x ∈ R x \in R x ∈ R b k ( x ) b_k(x) b k ( x ) A c c ( x ) = ⋁ q e n d S q e n d b k ( x ) Acc(x)=\bigvee_{q_{end}}S_{q_{end}}^{b_k(x)} A cc ( x ) = ⋁ q e n d S q e n d b k ( x ) s k s_k s k x ∈ R x \in R x ∈ R x ∉ R x \notin R x ∈ / R s k → A c c ( x ) s_k \to Acc(x) s k → A cc ( x ) s k → ¬ A c c ( x ) s_k \to \lnot Acc(x) s k → ¬ A cc ( x ) s k ∧ ( ⋀ j < k ¬ s j ) s_k \land \left(\bigwedge_{j<k} \lnot s_j \right) s k ∧ ( ⋀ j < k ¬ s j )
相（不）等约束编码细节 ：命题 ψ \psi ψ k k k ∣ w ∣ |w| ∣ w ∣ ( b k − 1 ( x ) , b k ( x ) ] (b_{k-1}(x),b_k(x)] ( b k − 1 ( x ) , b k ( x )] h x [ i ] a , w [ i ] , λ h_{x[i]}^a,w[i],\lambda h x [ i ] a , w [ i ] , λ
上界推算
设 h h h ψ \psi ψ h h h
首先考虑 normal form（整体是 CNF，每个元素都是不为字符串相等的原子约束）的字符串命题 φ \varphi φ x i x_i x i x i ∈ R x_i \in R x i ∈ R x i ∉ R x_i \notin R x i ∈ / R M i = ⋂ t = 1 k L ( R t ) ∩ ⋂ t = 1 l ( R t ′ ) ‾ M_i=\bigcap_{t=1}^k \mathcal{L}(R_t) \cap \bigcap_{t=1}^l \overline{(R'_t)} M i = ⋂ t = 1 k L ( R t ) ∩ ⋂ t = 1 l ( R t ′ ) Q i Q_i Q i M i M_i M i ∣ h ( x i ) ∣ ≤ ∣ Q i ∣ |h(x_i)| \le |Q_i| ∣ h ( x i ) ∣ ≤ ∣ Q i ∣ k k k x i ≠ w x_i \ne w x i = w
∣ h ( x i ) ∣ ≤ 2 k × ∣ Q 1 ∣ × ⋯ × ∣ Q n ∣ |h(x_i)| \le 2^k \times |Q_1| \times \dots \times |Q_n|
∣ h ( x i ) ∣ ≤ 2 k × ∣ Q 1 ∣ × ⋯ × ∣ Q n ∣
当然在实际实践中，可以先把命题拆成一些变量彼此独立的部分，以减小 ∣ Q i ∣ |Q_i| ∣ Q i ∣
针对可能存在的相等约束 x = w x=w x = w ∣ h ( x i ) ∣ = ∣ w ∣ |h(x_i)|=|w| ∣ h ( x i ) ∣ = ∣ w ∣ ψ ∧ x = w \psi \land x=w ψ ∧ x = w ψ ′ = ψ [ x = w ] \psi'=\psi[x=w] ψ ′ = ψ [ x = w ] ψ \psi ψ
Multi-Step IAM Attacks
USENIX 2023, Citi, Ilia Shevrin: Detecting Multi-Step IAM Attacks in AWS Environments via Model Checking
简介
本论文深度基于 AWS 的云上环境，深度建模了 IAM 的鉴权系统，并在此之上创新性地构建了云上多步提权攻击路径检测的 Bounded Model Checking。作者坦言当前的 BMC 是 not complete 的，即只能预设一个最大步长来聚焦短的攻击路径，没法像 k-induction 那样证明整个系统的安全性。实测发现步长 ≥ 5 \ge 5 ≥ 5
本论文除了构造了 Bool+Str 的常规 SMT 编码外，还提出了一种基于纯 Bool 的 SAT 编码（还原 Str 时需要 SMT 编码）。实验分别测试了同账号场景（资源个数分布在 200 ∼ 700 200 \sim 700 200 ∼ 700 5 ∼ 80 5 \sim 80 5 ∼ 80 200 200 200
IAM 鉴权建模
本论文有明确的威胁假设和覆盖场景，包括：攻击者必须从某个合法的 AWS 身份开始操作，攻击者知道账号或组织下的资源配置和资源名，攻击者仅通过 IAM 体系发起提权（而非网络等方式），切换委托没有时效等。
IAM 鉴权建模完全参照 AWS 对外公开的鉴权流程，下面展示了鉴权全流程图和身份策略鉴权逻辑图。本论文对 InvokeFunction 和 RunInstances 的建模处理和 AssumeRole 很接近，即这两个操作都可以达成目标身份的切换。UpdateFunctionCode 可以覆盖 Function 内容，就和 UpdateAssumePolicyRole 一样。
框架
整个提权建模就是个 BMC 框架。通过 AWS 的 GetAccountAuthorizationDetails 接口拿到详细的云上安全配置并做初始化。实验代码用 JAVA 开发，使用的 SMT 求解器后端是 Z3，通过 Z3 Java API 调用来建模。
SMT 转 SAT
值得一提的是论文提出的 String 约束转 Bool 约束的思路。将所有策略里的正则约束全部提权出来构成数组（字符串常量看作一种特殊的正约束），每个字符串变量就能转化成等长的布尔数组，表示是否满足当前正则约束。由于这个数组的顺序不重要，以下用 s t r [ r e g ] str[reg] s t r [ re g ] s t r str s t r r e g reg re g Algorithm 2 ）来构造真实串。
整个流程有个预处理（Algorithm 1 ），即两两枚举正则约束 ( r e g 1 , r e g 2 ) (reg_1,reg_2) ( re g 1 , re g 2 )
Incremental Inprocessing in SAT
SAT 2019, Johannes Kepler University, Katalin Fazekas: Incremental Inprocessing in SAT Solving , Slides
A billion SMT queries a day
CAV 2022 (Invited Paper), AWS, Neha Rungta: A billion SMT queries a day
Zelkova and Z3AUTOMATA
FMCAD 2018, AWS, John Backes: Semantic-based automated reasoning for AWS access policies using SMT
wechat
alipay
