Wednesday, April 1, 2020

Two Sample t-Test(T 檢定)概念入門

簡介
日常生活中,我們常常需要比較兩種數據的差別。例如,我們想比較 A 分店與 B 分店的銷售額,又或者在食品生產過程中,我們想比較不同日子生產的貨品,重量到底有沒有差別。近年來,機器學習的流行,令不少人也想找出,更改參數到底令系統有多少實際進步。

一般來講,不採用任何統計學的方法的話,我們可以用平均值來判斷。但採用這種方法,我們難以界定兩組數據,是否「有明顯差別」。特別是當兩組數據的方差不一,但平均值相同的時候,我們很容易下錯判斷,誤以為兩者完全相同(反之亦然)。所以,T 檢定可以運用統計學的原理,幫助我們系統化地檢驗兩個平均值是否真的相等。

例如在以下圖片中,有兩組不同數據,到底他們相差多少?若果 Factor Level 2 的方差再大一點,大得把 Factor Level 1 的平均值也包含在它的 Bell Curve 之內的話,這樣算不算「沒有明顯差別」? T 檢定正是針對以上的問題,提出一個系統化的解法。


條件
要使用 t-Test,首要條件必須是兩組數據都屬於常態分布 (two datasets are normally distributed)。而且,實驗必須以隨機順序方式 (randomized sequencing) 進行,否則結果將不準確,可能會有偏差 (bias)。

假定
原假定 (Null Hypothesis, H0) 是指「預期中的情況」,也就是兩個平均值一樣 ( μ1 = μ2 )
替代假定 (Alternative Hypothesis Ha) 是指「不在預料之中的情況」,有三種可能:
  1.  μ1 >  μ2(其中一種 two sided alternative hypothesis)
  2.  μ1 <  μ2(另一種 two sided alternative hypothesis)
  3.  μ1 !=  μ2 (one sided alternative hypothesis)
界定準則
要判斷兩者是否相等,需使用以下的標準:
  • P(Type I Error) = P(reject H0 | H0 is true) (也稱作 α 或 significance level)
    這是指「當 H0 是真實的情況下,你錯誤地否認 H0 的機會率」。當這個數字越高,反映著 H0 是真實的機率其實很高,或者你錯誤地否認 H0 的機率很高。相反,這個數字越低,代表 H0 很可能不是真實,或者你否認 H0 的決定並沒有錯。
  • P(Type II Error) = P(failed to reject H0 | H0 is false) (也稱作 β 或 1-Power)
    這是指「當 H0 是錯的情況下,你沒有否認 H0 的機會率」。當這個數字越高,反映著 H0 根本就是錯的機率很好,或者你沒有正確否認 H0 的機率很好。相反,這個數字越低,反映 H0 是錯的可能性很低,或者你做錯判斷的可能性很低。基本上來講,β 越低,反映整個研究的誤差(也就是誤判的機率)很低。
  • Power = 1 - β
    Power 越高,反映研究的誤差越低(也就是研究越 Powerful)。相反,越低代表誤差越大,可靠度越低。
標準公式
T 檢定有兩種:

第一種屬於 Pooled Test,是指研究數據並沒有分任何指定對象,每次都是隨機從彩池(所以就叫 Pool)中抽出來的數據,這種情況應用以下公式:
當中 S 是指從數據中計出來的方差,而 DOF 則會是 n1+n2-2。以上公式假設在理論環境之下,兩者的方差一致(也就是大部分情況)。如果實際上並非如此,或者你不能肯定以上假設的話,可應用另一公式,當中 v 是指 DOF:

第二種屬於 Paired Test,是指研究數據有分指定對象,兩組數據均由同一批人中抽取出來。這種測試特別對於減肥實驗、酒精測試等實驗十分重要:因為每個人的體質均有差別,使用 Paired 的方法可以有效減少不必要的外在因素。這種情況可用以下公式:


不理解公式原理亦無傷大雅,只需知道以上公式,主要是由 CLT 中推演出來即可。

判定是否相等
假設 Significance Level (α) 設定為 0.05,這是指「只要 H0 真實/我判錯的機會率低於 5%,我將會判定 H0 為可信」。首先,我們使用以上公式找出 t0,然後根據 t0 及 DOF,查找 t distribution table 後,我們得出 p-Value。這個 p-Value 將會與 α 作比較:
  • 若 p-Value 大於 α,我們將斷定 H0 為不能否認,也就是承認 μ1 =  μ2,兩組數據相等。
  • 若 p-Value 少於或等於 α,我們將否認 H0,採納 Ha。
  • 若果情況為 Two-sided Test, α 需要除二,代表兩邊共享 α 的 5%,也就是每邊 2.5%。
使用電腦計算
知道以上基本概念,我們可以將所有數式交由電腦計算。主流而言,R/MATLAB/Python/SPSS 均有支援,但以 SPSS 圖形化界面的教學最多,其次是 MATLAB 的文檔最仔細。是次以 MATLAB 的文檔作示範,我們可以用 Two-sample T-Test (ttest2) 函數庫來進行計算:

首先,預備兩組資料:
load examgrades
x = grades(:,1);
y = grades(:,2);

執行 ttest2 算出 μ1 (from x) 與 μ2 (from y) 是否相等:
[h,p,ci,stats] = ttest2(x,y)

當中,h=0 指在默認 α=0.05 下,不能否認 Null hypothesis。

小結
使用 Two Sample t-Test 可以有系統地分辨兩組數據的相似度,所以,對於機器學習訓練等研究來講,特別有用。因為要評測神經網絡的性能,不能單看準確度,更要看當參數改變後,兩個結果有沒有顯著進步和差別,繼而找出最有影響力的參數,加以調整。

Friday, January 10, 2020

Scyther Formal Verification 入門與安全特性

1. 使用 Scyther 的動機
Scyther 是一套自動挖掘網絡協議 (Network Protocol) 漏洞的軟件。由於用手計算/用算式去推算漏洞的步驟十分繁複,系統性也不高,所以研究人員都偏向採用這類驗證工具(Formal Verification Tools)去找不同協議的問題。

Scyther v1.1.3 截圖

Scyther 屬於進程演算 (process calculi) 的驗證工具,特點在於每一個協議參與者均會有一個 Role(角色),而研究人員則只需要按著不同的角色去編寫程序。同類型的例子還有 AVISPA 和 ProVerif。相比起 rule-based 的 Tamarin Prover,Scyther 更簡單直覺,但壞處則是原生支援的算法也比 Tamarin 少。

---

2. Scyther 中的不同名詞

在進程演算的工具中,Agent 主要指「執行 Role 的代理人」,在 Scyther 中它的角色並不明顯。此外,Nonce 則指「一次性編碼」(number used once),大概就是 token 的意思。

另外,Scyther 的 Threat Model 是基於 Dolev-Yao Model。簡單來說,它指的是攻擊者對網絡有全權控制(包括但不限於截取信息、更改順序、修改信息內容、扮作信息接收者等)。但另一方面,它也假設了加密算法完全可靠(也就是說攻擊者唯一知道加密內容的方法,就是要找出密碼)。所以,這種假設專門針對協議上的邏輯問題,並排除了加密算法的漏洞、或者是電腦病毒、內鬼泄露機密等其他因素。

還有以下數個,在 Scyther 的協議中常見的 Role Terms:
  • Var - 變數名
  • Fresh - 新鮮變數名,會隨著建立新實體 (instantiation) 時派一個新的初始值
  • Role - 角色(例如 Alice 和 Bob)
  • Func - 函數名
  • sk(RoleTerm) / pk(RoleTerm) / k(RoleTerm, RoleTerm) - 密鑰(私鑰/公鑰/對稱)
  • pk(rt)^-1 = sk(rt) - 公鑰的 inverse key 就是私鑰,反之亦然
  • Run - 類似 Thread / Process 的概念,就是經過實體化(instantiation)的 Role。
  • RunTerm - 在 run 中的已實體化變數 
  • RunEvent - 將 Role 實體化成 Run 的事件 (Event)
  • Agents - 執行 Role 的代理人
  • RID - unique run identifier

而 Scyther 的基本文法也十分清晰:
  • send(R, R', rt) - 由 R 傳送到 R',內容為 rt
  • claim(R, c) - R 需要滿足 security claim c 
  • claim(R, secret, rt) - R 需要確保變數 rt 的機密性 (secret to adversary)

---

3. Scyther 中的不同驗證強度 (Aliveness / Synchronization / Agreement)
對方存在 Aliveness:
  • Weak Aliveness - 對方存在,且成功運行協議(假設對方絕對可信)
  • Weak Aliveness in the Correct Role - 對方存在,且身份正確(Alice 找 Bob,而非兩個 Alice)
  • Recent Aliveness - 對方近期存在,且成功運行協議(利用 token 確保對方未死)
  • Recent Aliveness in the Correct Role - 對方近期存在,且身份正確(確保 Alice 找到未死的 Bob)
成功同步 Synchronization:
  • Non-injective (non one-to-one) Synchronization - 成功運行整個協議(不會因被攻擊,以致只運行到一半)
  • Injective Synchronization - 成功運行整個協議,而且對方也是一對地成功運行
協議內容同步 Agreement:
  • Non-injective Agreement - 運行協議後,變數 (Variables) 得到預期的結果
  • Injective Agreement - 運行協議後,變數得到預期結果,而且只能一對一地運行(不能有 Intruder 先發送一個請求,然後 Alice 接手回應的情景) 
  • Weakagree - 所有協議執行者,均扮演著預期的角色。例如有三個人,他們知道自己是A,B 和 C,而其餘兩個人都正確知道,自己正在跟 B,C / A,C / A,B 對話。
安全強度表:

---

4. Scyther 的實例
參考 /scyther-mac-v1.1.3/Protocols/needham-schroeder-lowe.spdl
運行截圖:

---

Reference:

[1] The Scyther Tool - https://people.cispa.io/cas.cremers/scyther/index.html
[2] Operational Semantics and Verification of Security Protocols - https://www.springer.com/gp/book/9783540786351

Monday, January 6, 2020

Running Scyther Tool v1.1.3 on Mac OS X Catalina

The Scyther tool is a relatively simple protocol verification tool which performs formal verification of any security protocols. Although it may not be as powerful as Tamarin Prover, its relatively simple scripting language and GUI interface help learners to kick-start their project easily.

The Scyther tool should run seamlessly on older versions of Mac because of the older version of wxPython. However since Catalina, the libraries should have been updated, causing some issues while running the program.

Here explained some changes after my experiments:

1. Download Scyther Tool for Mac v1.1.3 here:
https://people.cispa.io/cas.cremers/scyther/index.html

2. Unzip and navigate to the terminal

3. run the following command:
python scyther-gui.py

4. Run some examples such as NSPK:
https://github.com/cascremers/scyther/blob/master/gui/Protocols/needham-schroeder.spdl

5. Check if you experienced some errors like this:
  File "/Users/chriz/Desktop/scyther-mac-v1.1.3/Gui/Attackwindow.py", line 96, in update
    (framewidth,frameheight) = self.GetClientSizeTuple()
AttributeError: 'AttackDisplay' object has no attribute 'GetClientSizeTuple'

  File "/Users/chriz/Desktop/scyther-mac-v1.1.3/Gui/Attackwindow.py", line 121, in update
    if not bmp.Ok():
AttributeError: 'Image' object has no attribute 'Ok'

If so, change the following two lines in Gui/Attackwindow.py:

Line 96:
- (framewidth,frameheight) = self.GetClientSizeTuple()
+ (framewidth,frameheight) = self.GetClientSize()
Line 121:
- if not bmp.Ok():
+ if not bmp.IsOk():

6. After modifying the code above, re-run the Step 3.
Although there are still some other errors, it should at least run with patterns successfully shown.

Screen Capture:


---

Reference:

https://wxpython.org/Phoenix/docs/html/classic_vs_phoenix.html
https://wxpython.org/Phoenix/docs/html/wx.Image.html