數據流值滿足半格的定義，以及數據流方程中的傳遞函數滿足單調性

在滿足正確性的前提下，當數據流值對應的半格高度有限時，必定收斂。以最小元為初值的迭代收斂于最小不動點，以最大元為初值的迭代收斂于最大不動點

IDEAL是理想解即最精確的解，它將程序入口entry到某點p所有可達路徑（可執行路徑）的尾端的數據流值做聚合操作，區分來自不同路徑的數據流值，若聚合操作是交運算，則最大下界為其值，任何大于IDEAL的解都是錯誤的，而小于IDEAL的解是保守的；若聚合操作是并運算，則最小上界為其值，任何小于IDEAL的解都是錯誤的，而大于IDEAL的解是保守的。MOP是全路徑聚合解，它將entry到p所有流圖路徑（不一定可執行）的尾端的數據流值做聚合操作，區分來自不同路徑的數據流值，若包含了不可執行路徑，則會丟失精確性，否則等于IDEAL；MFP是基于數據流方程與迭代算法求得的最大或最小不動點解，它在每個控制流圖的匯合節點做聚合操作而非路徑尾端，不區分來自不同路徑的數據流值，若傳遞函數不滿足分配律，則會丟失精確性，否則等于MOP。故精確性關系為MFP<=MOP<=IDEAL，可知MFP解是安全的，基于MFP作的優化是正確的

因為一般程序路徑數可能無限，所以沒有求MOP的有效算法，且不可達路徑是一個不可判定問題，所以沒有求IDEAL的有效算法

為什么要加寬算子？
因為當格的偏序集合L不滿足升鏈條件，從最小元迭代計算最小不動點的過程是不收斂的，即迭代序列(fⁿ(⊥))ₙ不保證最終穩定，且其最小上界不保證等于最小不動點，因此需要一種近似lfp(f)的方法。引入加寬算子fw:L×L—>L, fw(x)=x▽f(x)，可以將L上的一個序列轉為收斂的升鏈，從L的最小元開始迭代不斷上升，直至lfp(f)的一個上近似即fw的最小不動點lfp(fw)，關系式為lfp(f)<=f(lfp(fw))<=fw(lfp(fw))=lfp(fw)。對上式反復應用f單調得到：lfp(f)<=fⁿ⁺¹(lfp(fw))<=fⁿ(lfp(fw))<=…<=f(lfp(fw))<=lfp(fw)，這表明對lfp(fw)使用f迭代可獲得更精確的上近似，其過程可看成沿一個遞降鏈進一步逼近lfp(f)，但L不一定滿足降鏈條件而導致上述過程不收斂，故需要引入變窄算子fn:L×L—>L, fn(x)=x△f(x)，將L的一個序列轉為收斂的降鏈，從lfp(fw)開始迭代，不斷下降直至fn的一個不動點fp(fn)，則有關系式：lfp(f)<=fp(fn)<=lfp(fw)。注意，這里根據加寬算子的定義可知fw是單調的，但根據變窄算子的定義不確定fn是否單調，故從lfp(fw)迭代求得的fp(fn)，不確定是最小還是最大不動點，只能說是一個不動點，這也反映了變窄算子不需要滿足單調性，就可以更加逼近lfp(f)

1. 判定兩個完全格L和M能否構成伽羅瓦連接，即抽象化函數α: L—>M是否完全加性的，或具體化函數γ: M—>L是否完全乘性的

2. 構造抽象化函數和具體化函數，即對于一個Galois連接（L, α, γ, M），給定α可通過γ(m) = ⊔{l | α(l) ⊑ m}確定γ，這對于所有m成立，且由于α是確定的，因此γ是唯一確定的。取最小上界是為了保證m描述的L中元素對于所有安全地描述了M中α(l)的l是安全的；給定γ可通過 α(l) = ⊓ {m | l ⊑ γ(m) } 確定α，其唯一性和取最大下界的原因類似前面

3. 幫助定義分析具體格源值到抽象格屬性的正確性關系與表示函數。設有Galois連接（L, α, γ, M），R: V×L —>{true, false}為正確性關系，由表示函數β:V—>L生成，定義S: V×M —>{true, false}，則有v S m ⇔ v R (γ(m)) ⇔ β(v ) ⊑ γ(m) ⇔ (α◦β)(v) ⊑ m，即S為正確性關系，由表示函數α◦β: V—>M生成

4. 抽象化上迭代多次具體化+抽象化，結果等于一次抽象化，即α◦γ◦α = α；具體化上迭代多次抽象化+具體化，結果等于一次具體化，即γ◦α◦ γ = γ。這個性質被用于基于約化算子構造的伽羅瓦插入（特殊的伽羅瓦連接：具體化為單射，抽象化為滿射）的證明

分三大類，即順序組合、并行組合和函數空間。為簡化描述，下文簡稱Galois為G

1. 順序組合：取第一個G連接的具體格，最后一個G連接的抽象格，從第一個G連接到最后一個G連接組合各抽象化函數，從最后一個G連接到第一個G連接組合各具體化函數。例如，設（L₀, α₁, γ₁, L₁）和（L₁, α₂, γ₂, L₂）都是G連接，則（L₀, α₂◦α₁, γ₂◦γ₁, L₂）也是一個G連接

2. 并行組合：有六種方法，即獨立特征、相關性、直積、直張量積、約化積、約化張量積，前兩種用于組合分別針對不同結構多個分析的多個G連接為一個G連接。中間兩種組合針對同一結構多個分析的多個G連接為一個G連接，后兩種組合針對同一結構多個分析的多個G連接為一個G插入。獨立特征、直積、約化積與其它方法的區別是兩對抽象化函數與具體化函數之間沒有相互作用，會損失分析結果精度，本質就是P(A)×P(B)和P(A×B)的差別（P為冪集，A、B為集合）；獨立特征與直積、約化積的區別是具體化函數定義不同（抽象化函數相同），前者是兩個具體化函數的二元組即γ(m₁, m₂)=(γ₁(m₁), γ₂(m₂))，后者則是最大下界即γ(m)=γ₁(m₁)∧γ₂(m₂)

3. 函數空間：分為總函數空間和單調函數空間。對于前者，設（L, α, γ, M）為一個G連接，S為一個集合，f為S到L的函數，g為S到M的函數，因L和M為完全格，故由f或g構成的函數集合為總函數空間，則得到一個G連接（S—>L, α', γ', S—>M），其中α'(f)=α◦f, γ'(g)=γ◦g。對于后者，設（L₁, α₁, γ₁, M₁）和（L₂, α₂, γ₂, M₂）為G連接，f為L₁到L₂的函數，g為M₁到M₂的函數，因每個L及M為完全格，故由f或g構成的函數集合為單調函數空間，則得到一個G連接（L₁—>L₂, α, γ, M₁—>M₂），其中α(f)=α₂ ◦f ◦γ₁，γ(g)=γ₂◦ g◦ α₁

當要做數據流分析的一個完全格L不滿足升鏈條件時，除了直接對L運用加寬算子及變窄算子外，還怎么去計算近似它的最小不動點？這時伽羅瓦連接就派上用場了，先將L對應到另一個完全格M，即構造一個Galois連接或插入（L, α, γ, M），設A是L上的廣義單調框架（不要求L滿足升鏈條件，指定傳遞函數集合F為L到L的單調函數空間，即F本身也是完全格），其中f是L到L的單調函數，B是M上的廣義單調框架，其中g是M到M的單調函數，保證g是由f衍生的函數的上近似即α◦f◦γ ⊑ g，及M滿足升鏈條件。到了這里可以證明兩個結論：

? lfp(f) ⊑ γ(lfp(g)) 和 α(lfp(f)) ⊑  lfp(g)

?B的約束解(B₁, B₂)蘊含A的約束解(A₁, A₂)=(γ◦B₁, γ◦B₂)，下標1、2表示流圖結點的入口、出口。接下來有兩種方法可以計算近似L的最小不動點

1. 直接計算M上的最小不動點，然后應用上述結論?，取lfp(f) = γ(lfp(g))

2. 構造M的上界算子（針對Galois連接）或加寬算子（針對Galois插入），滿足 l₁ ∇ₗ l₂ = γ(α(l₁) ∇ₘ α(l₂))，可以證明左式為L上的一個加寬算子，取其lfp∇ₗ (f)。如果前面構造的是Galois插入，那么可以證明L和M兩者的加寬算子精度是一樣的，即lfp∇ₗ (f) = γ(lfp∇ₘ(α◦f◦γ ))

定理：集合Z[n]由所有i=0,1,…, n-1整數組成，其中滿足gcd(i,n)=1的元素與乘法模n操作形成了交換群G，且單位元為e=1。

證明：設a、b屬于G，有gcd(a,n)=1，gcd(b,n)=1，則gcd(a*b,n)=gcd(b,n)=1，即(a*b) mod n封閉，顯然單位元為1；根據擴展歐幾里德算法得a*x+n*y=1，x為a的逆元，則1=gcd(a,n)=gcd(a*x,n)=gcd(x,n)，故x也在G中

記輸出為[G`, G, p, q, g]，其中p為大素數，G`為模p的有限循環整數群，階為p-1；q為大素數，為G的階，G為G`的子群（模亦是p），生成元為g（G`的一個元素），另外滿足如下條件：

1. 1<q的位長<p的位長，p、q隨機選取，p同余于1 mod q，即q整除p-1，q為p-1的素因子

2. 1<g<=p-1，隨機選取，測試它的(p-1)/q次冪是否等于1 mod p，若等于則重新選取，直到不等于

3. 上面選定的g，遍歷1到q的冪模p，就得到G的各元素

數學基礎：一個有限群，對每個元素它的階整除群的階，它的群階冪次方等于單位元；一個有限循環群，它的生成元個數為群階的歐拉數，若群階是素數，則所有非1的元素都是生成元

結論：這種計算子群的方法由于保證階為素數且只要超過160位長，就可避免針對階為合數的質因子分解并利用中國剩余定理求離散對數的已知最好攻擊，具有中長期安全強度

定理：令K[x]是由次數小于8、系數為0或1的多項式組成的環，m(x)=x^8+x^4+x^3+x+1為不可約多項式，則K[x]/(m(x))（模m(x)剩余類環）同構于元素個數為256的有限域F

證明：

​1. 構造映射H: P->Z，P表示K[x]中的多項式，Z表示小于256的非負整數，定義函數h(p)=z(mod 256)。顯然H為雙射；依初等數論同余性質有h(p1+p2)=(z1+z2)mod 256=z1(mod 256)+z2(mod 256)=h(p1)+h(p2)，h(p1*p2)=z1*z2(mod 256)=z1(mod 256)*z2(mod 256)=h(p1)*h(p2)，故H保持加法乘法封閉性。這點保證支持任意明文/密文的運算

​2. 由一元多項式環的性質得多項式乘法可以交換，即f(x)•g(x)=g(x)•f(x)，滿足域的交換條件。其乘法單位元是常數項1，滿足域的單位元條件

​3. 因非零多項式f(x)與m(x)互素，由一元多項式環的互素定理知存在g(x)、k(x)使得f(x)•g(x)+m(x)•k(x)=1(系數模2)，即f(x)•g(x)模m(x)余1（這里1表示單位元），故f(x)存在逆元，由群定義知逆元必唯一，滿足域的逆元條件。另aes規定零多項式的逆元為其自身。這點保證s盒及列混合操作可逆

目錄


下載：基于Rust構建WebAssembly

  如果對于任意0<=a<p和0<=b<q(p和q皆是素數)，那么當x<p*q時，存在一個唯一的x，使得x≡a mod p 且 x≡b mod q，則

   x =(((a - b)*u) mod p)*q + b，其中u滿足u*q≡1 mod p。

1.先推導x的解

   因x≡a mod p 且 x≡b mod q

   故令x = k1*p + a 且 x = k2*q + b                     (1)

   即 k1*p + a = k2*q + b

     => a - b = k2*q - k1*p                                  (2) 

   又因u*q≡1 mod p，故令u*q = 1 + k3*p              (3)

   由(2)和(3)式

     => a - b = k2 * (1+k3*p)/u - k1*p

   兩邊同時乘u

     =>（a - b) * u = k2*(1+k3*p) - k1*p*u

   兩邊同時模p

     => ((a - b) * u) mod p = (k2 mod p) mod p     (4)

  

   又因x < p*q，故b + k2*q < p*q

    => b <(p - k2) * q

   因0<b<q，故p > k2

    => (k2 mod p) mod p = k2

   故(4)式即

     ((a - b) * u) mod p = k2                                  (5)

   將(5)代入(1)式可得

     x = (((a - b)*u) mod p)*q + b

2. 再證明x是唯一解

    假設x1是另一解，即 x1≡a mod p 且 x1≡b mod q，得

      x1 - x ≡ 0 mod p 即 p | x1 - x

      x1 - x ≡ 0 mod q 即 q | x1 - x

    又因p和q皆為素數，故p*q | x1 - x，得

      x1 - x ≡ 0 mod (p*q)

    故 x1 mod (p*q) = x mod (p*q)   證畢

 1 int redis_auto_connect(CBED_REDIS *redis)
 2 {
 3     if(NULL==redis->ctx){
 4         redisContext *ctx;
 5         if(redis->type == CONN_TCP)
 6             ctx = redisConnectWithTimeout(redis->conn.tcp.ip, redis->conn.tcp.port, redis->timeout_conn);
 7         else
 8             ctx = redisConnectUnixWithTimeout(redis->conn.unix.path, redis->timeout_conn);
 9         
10         if(NULL==ctx){
11             zlog_fatal(c_redis, "redis allocate context fail");
12             return -1;
13             
14         }else if(ctx->err){
15             zlog_fatal(c_redis, "redis connection %s:%d error: %s", 
16                         redis->type==CONN_TCP?redis->conn.tcp.ip:redis->conn.unix.path, 
17                         redis->type==CONN_TCP?redis->conn.tcp.port:0, ctx->errstr);
18             redisFree(ctx);
19             return -1;
20         }
21         
22         if(REDIS_ERR==redisSetTimeout(ctx, redis->timeout_rw)){
23             zlog_fatal(c_redis, "redis set rw timeout error: %s", ctx->errstr);
24             redisFree(ctx);
25             return -1;
26         }
27         
28         redis->ctx = ctx;
29         if(redis_auth(redis)){
30             redisFree(ctx);
31             redis->ctx = NULL;
32             return -1;
33         }
34         
35     }    else if(!(redis->ctx->flags & REDIS_CONNECTED)){
36         int retry = redis->reconn_max, n = 0;
37         do {
38             if(REDIS_OK==redisReconnect(redis->ctx)){
39                 return redis_auth(redis);
40             }
41             
42             zlog_warn(c_redis, "redis reconnect %d error: %s", ++n, redis->ctx->errstr);    
43             sleep(redis->reconn_interval); //reconn_interval default is 3 seconds
44             
45         }while(--retry > 0);
46         
47         zlog_error(c_redis, "redis reconnect exceed max num %d", redis->reconn_max);
48         return -1;
49     }
50 
51     return 0;
52 }

 1 static int redis_bulk_get_reply(CBED_REDIS *redis)
 2 {
 3     redisReply *r;
 4     int i = 0;        
 5     int num = redis->cmd_num;
 6     redis->cmd_num = 0;
 7 
 8     for(; i<num; ++i){
 9         if(REDIS_OK==redisGetReply(redis->ctx, (void**)&r)){
10             if(r->type == REDIS_REPLY_ERROR){
11                 zlog_error(c_redis, "redis get reply error: %.*s", r->len, r->str);
12                 freeReplyObject(r);
13                 return -1;
14             }
15             freeReplyObject(r);
16         
17         }else{
18             if(redis->ctx->err==REDIS_ERR_IO||redis->ctx->err==REDIS_ERR_EOF)
19                 redis->ctx->flags &= ~REDIS_CONNECTED;
20             zlog_fatal(c_redis, "redis get reply fail: %s", redis->ctx->errstr);
21             return -1;
22         }
23     }
24 
25     return 0;
26 }
27 
28 int redis_send(CBED_REDIS *redis, unsigned char *data, unsigned int size, int force)
29 {
30     if(redis_auto_connect(redis))
31         return -1;
32 
33     int i;
34     
35     if(redis->max_cmd_num > 1){ //pipelining
36         for(i=0; i<redis->queue_num; ++i){
37             if(REDIS_ERR == redisAppendCommand(redis->ctx, "RPUSH %s %b", redis->queue[i], data, size)) {
38                 zlog_fatal(c_redis, "redis append command rpush %s len %u fail: %s", redis->queue[i], size, redis->ctx->errstr);
39                 return -1;
40             }
41             
42             ++redis->cmd_num;
43             if((!force && redis->cmd_num==redis->max_cmd_num) || force){
44                 if(redis_bulk_get_reply(redis))
45                     return -1;
46             }
47         }
48         
49     }else{
50         for(i=0; i<redis->queue_num; ++i){
51             redisReply *r = redisCommand(redis->ctx, "RPUSH %s %b", redis->queue[i], data, size);
52             if(NULL==r){
53                 if(redis->ctx->err==REDIS_ERR_IO||redis->ctx->err==REDIS_ERR_EOF)
54                     redis->ctx->flags &= ~REDIS_CONNECTED;
55                 zlog_fatal(c_redis, "redis command rpush %s len %u fail: %s", redis->queue[i], size, redis->ctx->errstr);
56                 return -1;
57             }
58             
59             if(r->type == REDIS_REPLY_ERROR){
60                 zlog_error(c_redis, "redis reply rpush %s len %u error: %.*s", redis->queue[i], size, r->len, r->str);
61                 freeReplyObject(r);
62                 return -1;
63             }
64 
65             freeReplyObject(r);
66         }
67     }
68 
69     return 0;
70 }