goo foo
R SSA Path-1
M1_s_0 = @parameter0
(M1_s_0.matches("[A-Z][^a-z]+"))
M1_s_0 = @parameter0 Sink Point : No
M1_s_0 = @parameter0
Figure 4.15 Intra Path constraints collection of idCheck method
句中有定義，這些變數定義的語句也要蒐集進來才能確保路徑限制資訊的完整，
其中要蒐集回傳值語句是因為之後跨程序路徑限制蒐集的需要，而分支語句的條 件式才是我們要整個路徑限制蒐集的主角。採用反向的原因在於方便我們蒐集這 些變數定義的語句，因為程式的邏輯都是先定義變數，才能使用變數。
我們先以 SSA Path-1 來作程序內路徑限制蒐集，可以看到對於每條 SSA 路 徑我們都會有一個對應的路徑限制(Path Constraint)容器來儲存符合條件的語句，
在此為 PC-1，從圖中可以看到我們對路徑上的語句都有作標籤因此可以清楚的 分辨語句的類型。首先反向蒐集先遇到回傳值語句 return M1_s_0，是我們的目 標之一所以蒐集到 PC-1，同時也將變數 M1_s_0 記錄起來，表示後面我們對於定 義 M1_s_0 的語句也要作蒐集。接著往上一個語句為分支語句 M1_s_0.match- es("[A-Z][^a-z]+")，一樣要蒐集到 PC-1，其中使用的變數 M1_s_0 剛已經記錄過，
所以在接著往上一個語句為變數 M1_s_0 的定義語句 M1_s_0 = @parameter0(其 中@parameter0 代表函式的第一個參數)，所以也要蒐集到 PC-1，就完成了 SSA Path-1 路徑限制的蒐集，最後 PC-1 就為函式 idCheck 的一條蒐集好的路徑限制。
在每個路徑限制上我們還會多記錄是否為包含弱點的路徑限制，也就是如果原本 SSA 路徑是包含接受點語句(Sink statement)的路徑，再產生對應的路徑限制就會 再記錄是否包含接收點，SSA Path-1 的路徑中沒有包含接收點語句，所以可以看 到 PC-1 的最上面有記錄 Sink point 為 No，而整個程序內路徑限制蒐集的流程就 如上述。以此類推，Figure 4.15 為函式 idCheck 中所有路徑最後蒐集完成後，產 生對應的 PC-1 和 PC-2。在蒐集完函式產生的路徑限制之後，依照存放的容器順 序，將路徑限制存放到對應的路徑限制集，在將路徑限制集存到路徑限制表中，
Figure 4.16 函式 idCheck 產生的路徑限制 PC-1、2 會存在對應的限制集 PCSet-1，
再依據 idCheck 的函式 ID 為 M1 存入路徑限制表中。
4-1-2-3-2 跨程序路徑限制蒐集
基本上跨程序路徑限制蒐集是包含程序內路徑限制蒐集的蒐集規則，只是多了呼
我們以 Figure 4.16 函式 doGet 的 SSA Path-1 作為跨程序路徑限制蒐集的說明。
因為只有在對呼叫外部函式語句(Call out statement)的部分有所不同，所以我 們直接說明跨程序路徑限制蒐如何處理呼叫外部函式語句。從 Figure 4.16 可以 看到 SSA Path-1 遇到的呼叫外部函式語句為 idCheck 函式，因此我們根據 idCheck 的函式 ID 去查詢路徑限制表可以找到對應 idCheck 函式的路徑限制集 PCSet-1，
其中包含兩條路徑限制，我們會分別對這兩條路徑限制進行合併的動作以達成完 整完的路徑限制蒐集。從這裡我們可以知道 SSA Path-1 會再拆分成兩條路徑限 制，Figure 4.17 為我們對 PCSet-1 的第一條路徑限制作為合併範例的說明，合併 主要分成兩個動作，一個是參數與引數的對應(Parameter and Argument Matching)，
將 參 數 對 應 到 引 數 ， 圖 中 可 以 看 到 PC-1 中 包 含 參 數 的 語 句 M1_s_0 =
@parameter0，而 M0_id_0 為呼叫端的語句 M0_id_1 = idCheck(M0_id_0)的引數，
對應後產生新的語句 M1_s_0 = M0_id_0；第二個動作為回傳值的對應(Return value Matching)，其中路徑限制 PC-1 的回傳值為 M1_s_0，從呼叫外部函式語句
Path Constraint Table MID
M0_req_0 = @parameter0 M0_resp_0 = @parameter1
M0_name_0 =M0_ req_0.getParameter("name");
M0_id_0 = M0_req_0.getParameter("id");
M0_writer_0 = M0_resp_0.getWriter();
(M0_id_1.length() >= 5)
B
M0_id_1 = idCheck(M0_id_0);
C
(M0_name_0.length() >= 5)
B
M0_writer_0.println( M0_id_0);
S
Figure 4.16 Inter path constraints collection of Call out statement
M0_id_1 = idCheck(M0_id_0)可以知道變數 M0_id_1 要對應到函式 idCheck 的回 傳值，因此作對應後產生新的語句 M0_id_1 = M1_s_0，在兩個動作完成後，接 著將 PC-1 中其他的路徑限制也包含進來，則完成呼叫外部函式語句的跨程序路 徑限制合併。此合併的動作有點類似函式的內聯化(inlining)的動作，概念是遇到 外部呼叫函式時，將此函式預先蒐集好的路徑限制合併進來以完成跨程序路徑限 制蒐集的完整性，從圖中可以看到最後得到的三個語句就是合併後的結果，也就 是我們要蒐集到路徑限制的語句。
在了解對外部呼叫函式語句路徑限制蒐集的方法後，我們一樣以反向的順序 對函式 doGet 的 SSA Path-1 進行跨程序路徑限制蒐集。與程序內路徑限制蒐集相 同，遇到分支語句和回傳值語句就蒐集起來，遇到呼叫外部函式語句就作上述的 合併處理，並將產生的語句都蒐集起來。Figure 4.18 為函式 doGet 的 SSA Path-1 經過跨程序路徑蒐集之後，doGet 的路徑限制 PC-1 蒐集的一條完整的路徑限制，
其中一開始蒐集就遇到的接收點語句，雖然沒有要蒐集但表示我們的路徑限制是 包含弱點的路徑限制，因此我們要將此資訊紀錄起來所以路徑限制 PC-1 紀錄
M0_id_1 = idCheck(M0_id_0);
C
Sink Point : No
PC-1
(M1_s_0.matches("[A-Z][^a-z]+")) B
return M1_s_0;
R
M1_s_0 = @parameter0 M1_s_0 = M0_id_0
M0_id_1 = M1_s_0
M1_s_0 = M0_id_0
M0_id_1 = M1_s_0
(M1_s_0.matches("[A-Z][^a-z]+")) B
Parameter &
Argument Matching
Return value Matching
Figure 4.17 Call out method path constraint Inlining
在了解整個反向路徑限制蒐集的方法之後，回顧函式 doGet 由路徑辨識與分 析階段會得到 5 條路徑分別為 Path-1、2、3、4、6，從中我們以 Path-1 為例並展 示作 SSA 轉換後得到的 SSA Path-1，接著再利用 SSA Path-1 作反向路徑限制蒐 集得到最後路徑限制蒐集的結果。以此類推對其餘的路徑作 SSA 轉換得到 SSA Path-2、3、4、6 再接著作反向路徑限制蒐集的處理之後，函式 doGet 最後會產 生 5 條路徑限制，其中 2 條是由 SSA Path-1 產生的。由 Figure 4.16 可以知道因 為路徑 SSA Path-1 包含呼叫外部函式 idCheck，而 idCheck 有包含兩條路徑限制，
所以最後會得到兩條路徑限制，而且這兩條路徑限制都是包含弱點的路徑，也就
M0_req_0 = @parameter0 M0_resp_0 = @parameter1
M0_name_0 =M0_ req_0.getParameter("name");
M0_id_0 = M0_req_0.getParameter("id");
M0_writer_0 = M0_resp_0.getWriter();
(M0_id_1.length() >= 5)
B
M0_id_1 = idCheck(M0_id_0);
C
(M0_name_0.length() >= 5)
B
M1_s_0 = M0_id_0
M0_id_1 = M1_s_0
(M1_s_0.matches("[A-Z][^a-z]+")) B
M0_req_0 = @parameter0 M0_resp_0 = @parameter1
M0_name_0 =M0_ req_0.getParameter("name");
M0_id_0 = M0_req_0.getParameter("id");
(M0_id_1.length() >= 5)
B
(M0_name_0.length() >= 5)
B
Sink point : Yes PC-1
M0_writer_0.println(M0_id_0);
S
Figure 4.18 Collected Path constraint after Inter Path constraint collection
4-1-3 路徑限制解(Solving path constraints&Path constraint solution)
在路徑限制解的部分，我們利用 Kaluza String Solver 這個路徑限制分析工 具[14]來解我們程式所有蒐集好的路徑限制。由於我們分析的是 SOOT 提供的 Jimple 程式碼，因此在解路徑限制之前，要先將 Jimple 形式的路徑限制轉換成符 合 Kaluza 路徑限制的形式。Kaluza 路徑限制的文法請見[附錄二]，以下我們將就 Jimple 路徑限制的文法與 Kaluza 路徑限制轉換規則分別說明。
Figure 4.19 為我們蒐集的 Jimple 路徑限制之文法，可以看到 JimpleCons 代 表整個蒐集的路徑限制，由零個以上的 JimpleCon 所組成，在此我們要先說明蒐 集好的路徑限制會以 CNF(Conjunction Normal Form)的形式作為最後路徑限制的 輸出。路徑限制上蒐集的每個分支語句(Branch statement)的條件式都是一個限制 (Constraint)，所以 CNF 形式呈現的方式就如 C1∩ C2 ∩ C3 ∩…,(其中 Ci代表第 i 的限制)，將所有的限制交集起來，代表每個條件都要符合才能解出正確的結果，
JimpleCons := JimpleCon JimpleCons |ɛ JimpleCon := JIfStmt | JAssignStmt JIfStmt := (Expr , Negate)
JAssignStmt := Var ‘=’ Expr
Expr := InvokeExpr | BinopExpr | UnopExpr | Literal InvokeExpr := (Base , ClassName , MethodName , Args) BinopExpr := Expr Bop Expr
UnopExpr := ‘!’ Expr Negate := ‘“!”’ | ‘“”’
Bop := ‘+’ | ‘-’ | ‘*’ | ‘/’ | ‘<’ | ‘<=’ | ‘>’ | ‘>=’ | ‘==’ | ‘!=’
Base := Literal Args := Arg Args | ɛ Arg := Literal
ClassName := Var MethodName := Var
Literal := Var | Num | ‘“Str”’ | Bool Var := /['a'-'z' 'A'-'Z']['0'-'9' 'A'-'Z' 'a'-'z' '_']*/
Num := /['-']?['0'-'9']+/
Bool := ‘true’ | ‘false’
Str := /[^”]*/
Figure 4.19 Jimple Constraint Grammar
因此作 Kaluza 格式轉換時可以知道限制之間都是交集的關係。基本上 JimpleCon 分成 JIfStmt 和 JAssginStmt。簡單的來說，JIfStmt 就是路徑限制，代表條件判斷 式，而 JAssignStmt 代表的是條件判斷式中變數的定義，其他文法定義的細節可 以從 Figure 4.19 得知，在此就不再贅述。
[[ ]] :: Jimple Constriant Grammar Kaluza Constraint Grammar
1. [[jimpleCon jimpleCons]] = [[jimpleCon]] [[jimpleCons]]
2. [[(expr, negate)]] = consID_0 := [[expr]]; consID_1 := ! consID_0; ASSERT(consID_1); ,if negate=”!”
3. [[(expr, negate)]] = consID_0 := [[expr]]; ASSERT(consID_0); ,if negate=””
//four cases of JAssignStmt //case of Var ‘=’ BinopExpr
4. [[var = binopExpr]] = [[var]] := [[binopExpr]];
//case of Var ‘=’ UnopExpr
5. [[var = unopExpr]] = [[var]] := [[unopExpr]];
6. [[expr1 bop expr2]] = ([[expr1]] bop [[expr2]]) 7. [[! expr]] = ! [[expr]]
//caes of Var ‘=’ InvokeExpr
8. [[var = (base, className, methodName, args)]] = [[var]] := [[base]] . ([[args]])0 ;,if className=
”Java.lang.string”&&methodName=”concat”
9. [[var = (base, className, methodName, args)]] = [[var]] == Len([[base]]); ,if className=
”Java.lang.string”&&methodName=”length”
10. [[var = (base, className, methodName, args)]] = IF([[var]]){ [[base]] \in CapturedBrack(/([[args]])0/,0);}
ELSE{},if className=”Java.lang.string”
&&methodName=”matches”
11. [[(base, className, methodName, args)]] = [[base]]_start >= 0; [[base]]_end <= L_[[base]];
[[base]]_end >= [[base]]_start;
L_[[base]] == Len([[base]]);
[[base]] := [[base]]_1 . [[base]]_Res;
[[base]]_start == Len([[base]]_1);
I_[[base]] := [[base]]_end – [[base]]_start;
I_[[base]] := [[base]]_Res;
[[base]]_start == ([[args]])0; [[base]]_start == ([[args]])1;
[[var]] == [[base]]_Res;,if className=
”Java.lang.string”&&methodName=”substring”
//case of Var ‘=’ Literal
12. [[var = literal]] = [[var]] == [[literal]]
13. [[arg args]] = [[arg]], [[args]]
14. [[var]] = methodID_var_number 15. [[num]] = num
16. [[bool]] = bool 17. [[“string”]] = “string”
Figure 4.20 Kaluza Constraint Generation Rules
有了路徑限制定義的文法之後，我們接著需要將 Jimple 的路徑限制轉換成 Kaluza 形式的路徑限制，才能夠藉由 Kaluza 此路徑限制分析工具來產生最終的 測試案例。因此，我們將轉換過程以 Figure 4.20 的 Kaluza Generation Rules 來表 示。規則 2、3 為路徑限制的轉換規則，分別代表條件成立和不成立兩種，其中 第二個規則的 consID 代表一個會自動產生不同路徑限制代號的函式。
規則 4～11 代表路徑限制中使用到的變數定義之轉換規則，規則 8～11 為 Java string 函式的規則轉換，其中([[args]])0、([[args]])1代表第一個和第二個引數，
以此類推。在此 Java string 函式我們只展示出 concat、length、matches、substring，
關於其他的 Java string 函式的改寫可以參考[14]，Figure 4.21 為 PC-1 經過 Figure 4.20 的規則作 Kaluza 格式轉換的結果。
16 M0_TMP_i0_0 == Len(M0_name_0);
17 M0_id_0 == VAR_0xINPUT_id;
18 M0_name_0 == VAR_0xINPUT_name;
M1_s_0 = M0_id_0
M0_id_1 = M1_s_0
(M1_s_0.matches("[A-Z][^a-z]+")) B
M0_req_0 = @parameter0 M0_resp_0 = @parameter1
M0_name_0 =M0_ req_0.getParameter("name");
M0_id_0 = M0_req_0.getParameter("id");
(M0_id_1.length() >= 5)
B
(M0_name_0.length() >= 5)
B
Sink point : Yes PC-1
分支語句 M0_id_1.length() >= 5，第 1～4 行為此分支語句轉換的結果。其中第 1 行 P0_0 := M0_TMP_i0_1 < 5，解讀為限制 P0 的預設條件 P0_0 紀錄函式 ID 為 M0 裡面的暫存變數 i0_1 小於 5，其中 TMP(Temp)代表為暫存變數的型態。而因 為 Jimple 預設將條件式以否定的方式呈現，所以我們在這看到的條件式為 < 不 是 >= ，所以在第 2 行我們會作條件否定的動作 P0_1 := !P0_0，第 3 行用 ASSERT(P0_1)去強迫 P0_1 的條件為真以達成原本分支語句 M0_id_1.length() >=
5 條件為真的轉換，而第 4 行為變數 M0_TMP_i0_1 的定義，其中 Len(M0_id_1) 則代表 M0_id_1.length()的解讀。說明完第一個限制 P0 之後，繼續以反向的順序 隨著路徑限制 PC-1 作轉換，下個語句 M0_id_1 = M1_s_0 轉換在第 5 行，在下一 個語句為一個分支語句 M1_s_0.matches(“[A-Z][^a-z]+”)，轉換在第 6～11 行以此 類推，在最後 17、18 行看到的 VAR_0xINPUT 代表最後需要去解的使用者輸入變 數，在此 Kaluza 解出來結果為 VAR_0xINPUT_id='' D@P0@''、VAR_0xINPUT_name
= ''@@@@@''。