![](https://csdnimg.cn/release/download_crawler_static/88749558/bg5.jpg)
A. Banerjee
等人理论计算机科学电子笔记
173
(
2007
)
47
4
F-
保密 政策的完整性和满足性
等式(1)和(2)给了我们一种动态检查程序是否满足保密策略的方法:事实上,
这两个等式都使用了进程中程序的指称语义但是我们可以静态地做这个检查
我们现在将看到,静态检查涉及F-完备性,而不是B-完备性,并使用最弱的自
由前提,而不是指称语义。在最弱的自由主义前提下,(Wlp
P
写作
),方程
(1)具有以下等效的重新表述:
HWlp
P
H=Wlp
P
H (3)
等式(3)表明H对于Wlp
P
是F-完全的。换句话说:考虑通过H抽象具体的输入状态
X;这产生一组状态,其中
私有信息被抽象为“任何可能的值”。该等式断言Wlp
P
(H(X))是H的定点,这意
味着Wlp
P
(H(X))产生一组状态,其中每个公共输入与任何可能的私有输入相
关联:
定点的进一步抽象(参见,等式(3)的LHS)没有产生新的结果。因为
私有输入之
间没有区别
,所以公共输出独立于私有输入。因此,等式(3)断言标准NI。
下面的定理断言用B-和F-完备性描述不干涉的两种方法是等价的。
定理4.1 HP)
H
=
H
P)i
HWlp
P
H
=
Wlp
P
H
。
证据
由[11,12]我们知道,如果
f
是可加的,则对于任何
ρ
,我们有
ρ <$
f
<$ρ
=
ρ
<$
f
i <$ρ <$
f
+
<$ρ=
f
+<
$ρ。[4]我们有(P)
+
= Wlp
P
。分别取H
,
P)为ρ
,
f,我们
结束了
例
4.2
考虑规划
P
,令
VH
={0
,
1}×{0
,
1},
VL
={0
,
1}。
<$
P
):n
h
1
,
h
2
,
l
nn→n
h
1
,
h
2
,
lnn
12
12 13 14 15 16 17 18 19
P=
公共输出l总是1,因此P是安全的,如以下计算所示。给定V
H
×
{l}∈H,我们可以证
明对于<$P)的B-完备性成立:
H
(P)(
V
H
×{
l
}
))=
H
(
V
H
×{
1
}
)=
V
H
×{
1
}
=
H
(H
1
,
h
2
,
1
<$
)=
H
(P)
(
H
1
,
h
2
,
1
<$
))
Wlp
P
的F-完备性也成立
H
(
Wlp
P
(
V
H
×{
1
}
))=
H
(
V
H
×V
L
)=
V
H
×V
L
=
Wlp
P
(
V
H
×{
1
}
)
H
(
Wlp
P
(
V
H
×{
l
/
= 1
}
))=
H
(
H
)=
H
=
Wlp
P
(
V
H
×{
l
/
= 1
}
)