精品综合视频9,偷拍AV一区二区三区

Pre

在之前的文章中我簡(jiǎn)單的介紹了一種描述計(jì)算機(jī)安全常用的方式: Non-interference模型(GMNI)。再用一句話(huà)來(lái)回顧一下什么是non-intererence, 在一個(gè)系統(tǒng)中如果我們?nèi)サ羲械母甙踩斎?，系統(tǒng)的低安全等級(jí)輸出并不會(huì)發(fā)生任何變化。在這個(gè)模型的基礎(chǔ)上我們可以進(jìn)一步來(lái)定義什么樣的信息流是安全的(這里的信息流可以直接理解成數(shù)據(jù)流，即程序運(yùn)行中變量值變化的軌跡)。GMNI模型是要求程序是deterministic的，接下來(lái)所有的討論依然會(huì)只關(guān)心與程序終止無(wú)關(guān)的程序片段。

安全信息流

我們可以用如下方式更加詳細(xì)的描述程序中什么樣的數(shù)據(jù)流是安全的：

給定一個(gè)程序 $P$ , 其中變量集合 $H=\{h_1,h_2,..., h_n\}$ 是高安全等級(jí)變量， $L=\{l_1,l_2,....l_n\}$ 是低安全等級(jí)變量，稱(chēng)程序 $P$ 是安全的，當(dāng)且僅當(dāng)在程序終止時(shí) $L$ 中的變量的值不依賴(lài)與 $H$ 中變量的初始值。

在實(shí)踐中我們可以用給程序中的變量打上label的方式來(lái)標(biāo)記程序變量的安全等級(jí)。這里的label最簡(jiǎn)單的可以只有兩種安全等級(jí)，高和低。也有一些比較復(fù)雜的系統(tǒng)比如去Barbara Liskov的去中心化標(biāo)記模型(decentralized label model), 這個(gè)我會(huì)在后面的文章里面講(希望我能一直更新hhhh)。為了方便，本文只會(huì)討論最簡(jiǎn)單的label系統(tǒng)。

我們也可以用更加形式化的語(yǔ)言來(lái)描述：

給定一個(gè)程序 $P$ , 其中變量集合 $H=\{h_1,h_2,..., h_n\}$ 是高安全等級(jí)變量， $L=\{l_1,l_2,....l_n\}$ 是低安全等級(jí)變量，稱(chēng)程序 $P$ 是安全的，當(dāng)且僅當(dāng),對(duì)于任意store(就是變量到值的對(duì)應(yīng)關(guān)系)， $M_1,M_2$ 有 $M_1|_{H^c}=M_2|_{H^c}$ ,
$(\langle M_1,P \rangle \neq \bot ~ \wedge ~ \langle M_2,P \rangle \neq \bot ) \Rightarrow \langle M_1,P \rangle |_L = \langle M_2,P \rangle|_L$

其中記號(hào) $M|_X$ 表示一個(gè)store中只與變量集合X中有關(guān)的部分，比如 $M|_X=\{x \mapsto v | (x \mapsto v) \in M \wedge x \in X \}$ 。 $\bot$ 代表程序終止。

safety

通常來(lái)說(shuō)程序的安全性的定義與程序的執(zhí)行軌跡(trace)相關(guān)，就像在最原本GMNI模型中定義的那樣， Micheal Clarkson在Hyperproperties論文中展示了一個(gè)比較簡(jiǎn)潔直接的定義。

在這里我不想展開(kāi)講，后面單獨(dú)寫(xiě)hyperproperties的時(shí)候再仔細(xì)寫(xiě)
store和trace有很強(qiáng)的聯(lián)系，如果我們只看程序最終的store，那么可以得到如下的定義。

Pr是某一程序語(yǔ)言的程序集合，那么這種語(yǔ)言的安全性(safety)可以用如下的方式來(lái)描述：
對(duì)于 $S \subset Pr$ ,存在邏輯表達(dá)式 $\phi(X,Y)$ 滿(mǎn)足，
$S~=~\{P~|~\forall M.\langle M,P \rangle \neq \bot \Rightarrow \phi(\langle M,P \rangle ,M)\}$

這里不難看出安全數(shù)據(jù)流問(wèn)題邊并不是一個(gè)嚴(yán)格意義上的“安全問(wèn)題”。因?yàn)楹苊黠@的可以看到前面安全數(shù)據(jù)流的定義中我們是在對(duì) $M1,M2$ 兩個(gè)值進(jìn)行quantify，但是safety的定義中全稱(chēng)量詞只有一個(gè)。這一點(diǎn)在McLean 94年的A general theory of composition for trace sets closed under selective interleaving functions. 里面給了詳細(xì)的證明。

2-safety

在計(jì)算機(jī)安全中數(shù)據(jù)流安全是很重要的一種性質(zhì)，之前的討論已經(jīng)可以看出，數(shù)據(jù)流安全重點(diǎn)在于討論對(duì)于任意兩次不同的程序執(zhí)行，我們希望能夠的得到某種性質(zhì)。對(duì)于上面的safety定義我們可以稍稍修改就可以得到任意兩次版本的安全性質(zhì)：2-safety。

Pr是某一程序語(yǔ)言的程序集合，那么這種語(yǔ)言的安全性(safety)可以用如下的方式來(lái)描述：
對(duì)于 $S \subset Pr$ ,存在邏輯表達(dá)式 $\phi(X,Y,Z,W)$ 滿(mǎn)足，
$S~=~\{P~|~\forall M_1,M_2.(\langle M_1,P \rangle \neq \bot \wedge \langle M_2,P \rangle \neq \bot ) \Rightarrow \phi(\langle M_1,P \rangle ,\phi(\langle M_2, P \rangle, M_1, M_2)\}$

這種類(lèi)型的性質(zhì)還可以繼續(xù)推廣得到k-safety,就是為了分類(lèi)那些要對(duì)多條軌跡進(jìn)行quantify的那些性質(zhì)。這里的2啊，k啊的名字已經(jīng)慢慢的暗示我們，單純的性質(zhì)(property)可能還不能滿(mǎn)足我們對(duì)于程序運(yùn)行安全性質(zhì)的描述需求，我們需要對(duì)性質(zhì)再進(jìn)行抽象得到一種類(lèi)似二階性質(zhì)，也就是超性質(zhì)(hyperproperty)。

技巧： Self-Compose

如果我們希望對(duì)一種現(xiàn)實(shí)中存在的語(yǔ)言進(jìn)行數(shù)據(jù)流安全的驗(yàn)證，一種非常常見(jiàn)和直接的做法是，設(shè)計(jì)一個(gè)類(lèi)型系統(tǒng)，在這種類(lèi)型系統(tǒng)中，每一個(gè)變量的類(lèi)型中還需要加上label。Jif就是這種思路的一個(gè)非常好的實(shí)踐， Jif中的label系統(tǒng)還是比較復(fù)雜的，他就使用了我之前提到的decentrialized label model.通過(guò)類(lèi)型check，來(lái)自動(dòng)的驗(yàn)證程序中的信息流安全。這種方式擴(kuò)展了程序的類(lèi)型系統(tǒng)語(yǔ)義(Jif就是擴(kuò)展了Java的類(lèi)型系統(tǒng))。但是如果我們仔細(xì)觀察2-safety的定義，對(duì)于數(shù)據(jù)流安全這樣的2-safety問(wèn)題，既然是論證程序的兩次運(yùn)行，那么我們?yōu)槭裁床恢苯幼尦绦蚺軆纱文兀?strong>自組合(self-compose)就是這種思路最好的體現(xiàn)。

對(duì)于程序P, $V(P)$ 表示所有P中的變量，C(P)是對(duì)程序P的一個(gè)拷貝，其中所有的變量名全部替換為原來(lái)的變量名加上'.

S是是一個(gè)2-safety性質(zhì), 對(duì)于某個(gè)邏輯表達(dá)式 $\phi$ ,自組合規(guī)約可以定義為
$\{P' ~|~ P' = P ; C(P) \wedge \forall M_1, M_2. \langle M_1 \cup C(M_2), P' \rangle \neq \bot \Rightarrow \theta \}$
其中 $\theta =\phi (\langle M_1 \cup C(M_2), P' \rangle|_{V(P)}, \langle M_1 \cup C(M_2), P' \rangle|_{V(C(P))}, M_1,M_2)$

;代表程序順序執(zhí)行。

使用自組合可以重新定義信息流安全：

給定一個(gè)程序 $P$ , 其中變量集合 $H=\{h_1,h_2,..., h_n\}$ 是高安全等級(jí)變量， $L=\{l_1,l_2,....l_n\}$ 是低安全等級(jí)變量，稱(chēng)程序 $P$ 是安全的，當(dāng)且僅當(dāng), 對(duì)于任意store $M_1,M_2$ 有 $M_1|_{H^c}=M_2|_{H^c}$
$\langle M_1 \cup M_2,P;C(P)\rangle \neq \bot \Rightarrow, \langle M_1 \cup M_2,P;C(P)\rangle |_L ) = \langle M_1 \cup M_2, P;C(P) \rangle|_{C(L)}$

光看定義很復(fù)雜但是其實(shí)非常簡(jiǎn)單，用人話(huà)說(shuō)就是把一個(gè)程序復(fù)制一遍貼在原來(lái)的程序后面，然后把里面所有的變量名全都換成原來(lái)的名字加一撇，然后信息流安全就是說(shuō)假設(shè)輸入的時(shí)候所有的低安全級(jí)別的輸入都相同，程序最終結(jié)束的時(shí)候兩次運(yùn)行的低安全變量的結(jié)果相同

看個(gè)例子吧，原本的程序如下：

z := 1;
if (h) then x := 1 else skip;
if (?h) then x := z else skip;
l := x + y

其中變量h是高安全等級(jí)的變量，其他是低安全等級(jí)的變量。我們可以讓他跑兩次，self-compose一下：

z := 1;
if (h) then x := 1 else skip;
if (?h) then x := z else skip;
l := x + y;
z ′ := 1;
if (h′) then x′ := 1 else skip;
if (?h′ ) then x′ := z ′ else skip
l′ := x ′ + y′

這時(shí)候比如我們想要檢測(cè)l有沒(méi)有信息泄露我們只需要令程序運(yùn)行之前所有的除h外的變量和他們的復(fù)制變量都相等，最后結(jié)束的時(shí)候保證l=l'。從霍爾邏輯的角度來(lái)說(shuō)就是給一個(gè)前條件，{x=x',y=y',z=z',l=l'}, 后條件{l=l'}，驗(yàn)證一下就行。如果是用coq之類(lèi)的東西去做證明，這種方式比最原本的那個(gè)GMNI模型要容易很多。后面等空了我也會(huì)親自寫(xiě)一下再比較兩種方法證明上的差異。

其實(shí)這個(gè)例子還可以看出self-compose對(duì)于傳統(tǒng)使用類(lèi)型系統(tǒng)的方式是有一定的優(yōu)勢(shì)的。如果是傳統(tǒng)的使用label type這個(gè)程序是要被判定為不安全的，因?yàn)閘的值是要用到和h有關(guān)的分支中的值的，但是實(shí)際上由于我們對(duì)信息流的安全講的是一個(gè)最終的程序狀態(tài)，這個(gè)程序最終l不管h如何取值都是y+1。如果我們使用self-compose的方式，這種情況我們就可以給證出來(lái)是安全的。

Dafny是一個(gè)z3的wrapper，使用這個(gè)語(yǔ)言我們可以給程序增加前條件和后條件的方式，我們可以輕松的驗(yàn)證一下self-compose變換以后的測(cè)試程序

// test.dfy
method test(x:int,y:int,z:int, h:bool, hp:bool) returns (l: int, lp: int)
    ensures l == lp
{
  var x1 := x;
  var x2 := x;
  var y1 := y;
  var y2 := y;
  var z1 := z;
  var z2 := z;
  z1 := 1;
  if h {
    x1 := 1;  
  }
  else {
    x1 := z1;
  }
  l := x1 + y1;
  z2 := 1;
  if hp {
    x2 := 1;   
  }
  else {
    x2 := z2; 
  }
  lp := x2 + y2;
}

不出所料dafny接受了上面的程序，正常編譯。如果我們把原來(lái)程序中的z:=1替換成z:=2, self compose 變換后的dafny程序就會(huì)是

// test.dfy
method test(x:int,y:int,z:int, h:bool, hp:bool) returns (l: int, lp: int)
    ensures l == lp
{
  var x1 := x;
  var x2 := x;
  var y1 := y;
  var y2 := y;
  var z1 := z;
  var z2 := z;
  z1 := 1;
  if h {
    x1 := 2;  
  }
  else {
    x1 := z1;
  }
  l := x1 + y1;
  z2 := 1;
  if hp {
    x2 := 2;   
  }
  else {
    x2 := z2; 
  }
  lp := x2 + y2;
}

這一次 dafny 就會(huì)報(bào)錯(cuò)。說(shuō)名其中的信息流就不再安全了， l的值會(huì)和h有關(guān)。

1 A postcondition might not hold on this return path.

Reference

Barthe, G., D'argenio, P. R., & Rezk, T. (2004, June). Secure information flow by self-composition. In Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004. (pp. 100-114). IEEE.
Terauchi, T., & Aiken, A. (2005, September). Secure information flow as a safety problem. In International Static Analysis Symposium (pp. 352-367). Springer, Berlin, Heidelberg.
Myers, A. C., & Liskov, B. (1997). A decentralized model for information flow control. ACM SIGOPS Operating Systems Review, 31(5), 129-142.
Jif 3.0: Java information flow Software release, July 2006. Andrew C. Myers, Lantian Zheng, Steve Zdancewic, Stephen Chong, and Nathaniel
Clarkson, M. R., & Schneider, F. B. (2010). Hyperproperties. Journal of Computer Security, 18(6), 1157-1210.Leino, K. R. M. (2010, April).
Dafny: An automatic program verifier for functional correctness. In International Conference on Logic for Programming Artificial Intelligence and Reasoning (pp. 348-370). Springer, Berlin, Heidelberg.

色偷偷精品伊人,欧洲久久精品,欧美综合婷婷骚逼,国产AV主播,国产最新探花在线,九色在线视频一区,伊人大交九欧美,1769亚洲,黄色成人av

安全信息流與2-safety性質(zhì)

安全信息流與2-safety性質(zhì)

Pre

安全信息流

safety

2-safety

技巧： Self-Compose

Reference

相關(guān)閱讀更多精彩內(nèi)容

友情鏈接更多精彩內(nèi)容

色偷偷精品伊人,欧洲久久精品,欧美综合婷婷骚逼,国产AV主播,国产最新探花在线,九色在线视频一区,伊人大交九 欧美,1769亚洲,黄色成人av

安全信息流與2-safety性質(zhì)

Pre

安全信息流

safety

2-safety

技巧： Self-Compose

Reference

相關(guān)閱讀更多精彩內(nèi)容

友情鏈接更多精彩內(nèi)容

色偷偷精品伊人,欧洲久久精品,欧美综合婷婷骚逼,国产AV主播,国产最新探花在线,九色在线视频一区,伊人大交九欧美,1769亚洲,黄色成人av