2020年7月

使用Nginx反向代理Flask静态资源
环境:Ubuntu 18.04

实现原理

如果flask项目里面有大量静态资源,可以尝试使用Nginx代理对静态资源的请求,把真正的动态请求转发给Flask。

比如:
flask在127.0.0.1监听8001端口,而Nginx配置为监听0.0.0.0的8000端口,那么在外部请求hostname:8000时就会把动态请求转发到8001上,而静态资源请求则直接代理至储存静态资源的目录下。

Nginx配置

安装

apt install nginx

配置文件路径

  1. 存放全局配置:/etc/nginx/nginx.conf
  2. 存放单个server配置:/etc/nginx/conf.d/xxx-xxx-xxx.conf
    > 这个目录下的配置默认被1中的配置文件include了,所以可以单独编辑

* 注意Nginx配置文件的内层块是会继承外层块的属性的

具体配置内容

nginx.conf

  • 其中每个配置项都大有讲究,单这里重点标记反代flask要注意的
  • 如果在运行中改变了配置文件可以用nginx -s reload重载
#default: www-data
#这里要注意,运行nginx的用户需要和flask保持一致(这里个人原因用了root),否则会发生权限错误
user root;
worker_processes auto;
pid /run/nginx.pid;
include /etc/nginx/modules-enabled/*.conf;

events {
    worker_connections 768;
    # multi_accept on;
}

http {
    sendfile on;
    tcp_nopush on;
    tcp_nodelay on;
    keepalive_timeout 65;
    types_hash_max_size 2048;
    # server_tokens off;

    # server_names_hash_bucket_size 64;
    # server_name_in_redirect off;

    include /etc/nginx/mime.types;
    default_type application/octet-stream;

    ##
    # SSL Settings
    ##

    ssl_protocols TLSv1 TLSv1.1 TLSv1.2; # Dropping SSLv3, ref: POODLE
    ssl_prefer_server_ciphers on;

    ##
    # Logging Settings
    ##

    access_log /var/log/nginx/access.log;
    error_log /var/log/nginx/error.log;

    ##
    # Gzip Settings
    ##

    gzip on;

    # gzip_vary on;
    # gzip_proxied any;
    # gzip_comp_level 6;
    # gzip_buffers 16 8k;
    # gzip_http_version 1.1;
    # gzip_types text/plain text/css application/json application/javascript text/xml application/xml application/xml+rss text/javascript;

    ##
    # Virtual Host Configs
    ##

    include /etc/nginx/conf.d/*.conf;
    #include /etc/nginx/sites-enabled/*;
}

xxx-xxx-xxx.conf

  • 这个文件比较重要
server {
    listen      8000; # 对外监听的端口

    root        /root/github/Vision-Ward; #服务器上的项目目录
    server_name arm.eqqie.cn; # 域名

    # 处理静态资源:
    #注意这里用了正则表达式,也就是把路由到/static/*的请求都视为对静态资源的请求
    location ~ ^\/static\/.*$ { 
        #这里的root表示静态资源的位置,注意如果按照上面的写法,会在这个路径后拼接上static,所以这里只需要写到static的上层目录即可
        root /root/github/Vision-Ward/app;
    }

    # 动态请求转发到8001端口(gunicorn):
    location / {
        #flask监听的位置(不对外)
        proxy_pass       http://127.0.0.1:8001;
        #这里也很重要,把请求的原始信息暴露给藏在后面的flask,避免其没有办法获取用户真正的ip地址
        proxy_set_header X-Real-IP $remote_addr;
        proxy_set_header Host $host;
        #建议如果涉及非80端口请求重定向的时候,用下面这种设置,可以避免重定向后端口消失的问题
        #proxy_set_header Host arm.eqqie.cn:8000;
        proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for;
    }
}

flask配置

  • 注意监听地址保持和配置文件中proxy_pass一致
  • 然后只需要正常启动flask即可

使用nginx启动服务,如果遇到错误直接复制下来查就会有很多答案。也可以多注意看看log。

  • z3作为微软开发的求解器,其提供的接口在很多应用程序和编程语言中都可以使用。
    > z3prover在CHAINSAWNAVEX中均有使用
  • 在这里关键的作用是想要配和CodeQL,通过CodeQL提取路径约束,然后用Z3求解约束
  • 其实关于如何用CodeQL提取出可以作为z3输入的约束还是一头雾水...但是这不妨碍先学习z3的使用,说不定可以找到一些灵感完成两者的结合。(应该会有办法的,要不这条研究路线就断了)
  • 后期可能需要造一些轮子,这么说来还是需要花挺多时间的(尤其是假期即将结束,需要挺多时间复习开学期考功课)
  • 官方使用文档:https://rise4fun.com/z3/tutorialcontent/guide
  • z3py功能手册:https://z3prover.github.io/api/html/namespacez3py.html
  • z3py使用文档:https://ericpony.github.io/z3py-tutorial/guide-examples.htm
    > 如果二进制版的z3不便于后期结合,还需要花时间学下z3py
  • z3所使用的语法标准:http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
  • 最后,关于细节本文记录得不是很多,所以需要一些基础来阅读

环境安装

编译好的二进制版

  1. Github下载最新版:https://github.com/Z3Prover/z3/releases
    Z3prover
  2. 解压后将其中的bin目录添加到环境变量(Unix-like系统可以添加软连接到/usr/bin中)
  3. z3 <filename> 使用

z3py

  1. pip install z3-prover
  2. from z3 import * 使用
    > 注意在z3py中,很多语句被封装成了对象/类方法,但是基本求解逻辑还是一样的,取决于后期打算采用何种形式

基本语法

指令结构

z3指令有一套自己的结构,一般称为三地址码,其遵循的标准在引言中有链接。
基本的构成为 操作符 操作数1 操作数2

常量(constants)和函数(functions)

这是z3指令中最常见的两种结构,然而本质上常量只是作为一个没有参数的函数,其求解结果也以函数结构所表现。

(declare-fun f (Int) Int) ; 这里f是接受Int类型的函数
(declare-fun a () Int) ; a可以看成常量
(declare-const b Int) ; 语法糖写法,声明一个常量

与编程语言中函数不同的是,z3中的函数可以视为一个未解释的公式,不会在运行时抛出异常,也不会出现没有返回值的情况。专业术语将其称之为一阶逻辑或者谓词演算——百度百科。一阶逻辑中的“函数”是“未定义”的,意思就是不存在一种类似于四则运算一般固定的解释模式(model)。只要任何符合约束条件的model,都可以作为一种解释,而check-set就是用来求解的。

很抽象,可以看下面例子大概理解下。

用z3证明 f(f(x)) = x, f(x)=y, x!=y约束的存在性(给出一种可能性解释),并且还定义了一个抽象的类型(sort在z3中表示类型,使用declare-sort定义类型):

(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-fun f (A) A)
(assert (= (f (f x)) x))
(assert (= (f x) y))
(assert (not (= x y)))
(check-sat)
(get-model)
需要特别注意下z3函数的使用方式与编程语言不同:编程语言通过(x1,x2,x3)方式传参,而z3将函数视为一个运算符号通过类似三地址码的方式传参 —— 函数符号 x1 x2 x3

输出:

sat
(model
  ;; universe for A:
  ;;   A!val!0 A!val!1
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!0 () A)
  (declare-fun A!val!1 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!0) (= x A!val!1)))
  ;; -----------
  (define-fun x () A
    A!val!0)
  (define-fun y () A
    A!val!1)
  (define-fun f ((x!0 A)) A
    (ite (= x!0 A!val!1) A!val!0
      A!val!1))
)

生成的模型为A引入了抽象值。

算数运算

基本运算

z3内置了对于整数和实数等数学类型的支持,而且貌似最新版已经合并了原先的插件——z3str,可以进行字符串处理,关于这部分文档似乎没有详细说明...

declare-const可以用于声明整数和实数常量

如:

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)

声明完常量后,就可以在后续的式子中使用这些变量,式子中可以包含常用的数学运算符如:
+ - x div/mod/ram

check-sat & get-model

check-sat是高频使用的命令,用于对表达式求解,基本上就是为每个常数分配一个数字。如果存在一种解使得所有式子为真,那么结果就为sat,并且称这个解释为一个model,使用get-model可以查看;如果不存在解释,则结果为unsat,也无法获取可行的model。
例子:

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Real)
(declare-const e Real)
(assert (> a (+ b 2)))
(assert (= a (+ (* 2 c) 10)))
(assert (<= (+ c b) 1000))
(assert (>= d e))
(check-sat)
(get-model)

输出:

sat
(model
  (define-fun c () Int
    0)
  (define-fun b () Int
    0)
  (define-fun e () Real
    0.0)
  (define-fun d () Real
    0.0)
  (define-fun a () Int
    10)
)

类型转换

在z3中Int类型和Real类型不会自动互相转换,但是借助函数to-Real(参数为一个整数)可以将整数化为实数。
例子:

(assert (> e (+ (to_real (+ a b)) 2.0)))
(assert (= d (+ (to_real c) 0.5)))

非线性运算特性

当式子中有类似(* t s)的实数运算时称为非线性式,这种式子求解极其困难,导致z3在求解非线性问题的时候不一定总能确定是否有解。当无法确定是否可以求解时使用check-sat会返回unknow;当然,部分特殊的非线性式依然可以确定可满足性。
例子:

(declare-const a Int)
(assert (> (* a a) 3))
(check-sat)
(get-model)

(echo "Z3 does not always find solutions to non-linear problems")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)

(echo "yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...")
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(assert (= (* x x) (+ x 2.0)))
(assert (= (* x y) x))
(assert (= (* (- y 1.0) z) 1.0))
(check-sat)

(reset)
(echo "When presented only non-linear constraints over reals, Z3 uses a specialized complete solver")
(declare-const b Real)
(declare-const c Real)
(assert (= (+ (* b b b) (* b c)) 3.0))
(check-sat)
(get-model)

输出:

sat
(model
  (define-fun a () Int
    (- 3))
)
Z3 does not always find solutions to non-linear problems
unknown
yet it can show unsatisfiabiltiy for some nontrivial nonlinear problems...
unsat
When presented only non-linear constraints over reals, Z3 uses a specialized complete solver
sat
(model
  (define-fun b () Real
    (/ 1.0 8.0))
  (define-fun c () Real
    (/ 1535.0 64.0))
)

除法运算

z3支持除法、求模和求余运算,这些运算在底层都会被映射成乘法。

注意在实数除法的时候用符号/,因为实数没有求模和取余。

例子:

(declare-const a Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(declare-const r5 Int)
(declare-const r6 Int)
(assert (= a 10))
(assert (= r1 (div a 4))) ; integer division
(assert (= r2 (mod a 4))) ; mod
(assert (= r3 (rem a 4))) ; remainder
(assert (= r4 (div a (- 4)))) ; integer division
(assert (= r5 (mod a (- 4)))) ; mod
(assert (= r6 (rem a (- 4)))) ; remainder
(declare-const b Real)
(declare-const c Real)
(assert (>= b (/ c 3.0)))
(assert (>= c 20.0))
(check-sat)
(get-model)

输出:

sat
(model
  (define-fun c () Real
    20.0)
  (define-fun b () Real
    (/ 20.0 3.0))
  (define-fun r6 () Int
    (- 2))
  (define-fun r5 () Int
    2)
  (define-fun r4 () Int
    (- 2))
  (define-fun r3 () Int
    2)
  (define-fun r2 () Int
    2)
  (define-fun r1 () Int
    2)
  (define-fun a () Int
    10)
)

z3有一个很有意思的地方,就是不会发生除0错误,因为除0操作是未定义的,在求解的时候可以被定义为一个函数。
例如:

(declare-const a Real)
; The following formula is satisfiable since division by zero is not specified.
(assert (= (/ a 0.0) 10.0)) 
(check-sat)
(get-model)

; Although division by zero is not specified, division is still a function.
; So, (/ a 0.0) cannot evaluated to 10.0 and 2.0.
(assert (= (/ a 0.0) 2.0)) 
(check-sat)

输出:

sat
(model
  (define-fun a () Real
    1.0)
  (define-fun /0 ((x!0 Real) (x!1 Real)) Real
    10.0)
)
unsat

如果对上述行为不满意还可以使用ite语句自定义除法规则:

; defining my own division operator where x/0.0 == 0.0 for every x.
(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))
(declare-const a Real)
(declare-const b Real)
(assert (>= (mydiv a b) 1.0))
(assert (= b 0.0))
(check-sat)
关于ite语句:
其实就是if-then-else语句,其结构为(if 条件 真返回值 假返回值)
此处判断被除数是否为0来返回不同结果

位向量

暂略,用到的不多

数组

常用数组操作

  • 数组定义:(declare-const a1 (Array Int Int))

    这是使用了语法糖的定义方式,原生定义方式如下:

    (define-fun a1 () (Array Int Int) [val])
    例如:

    (define-fun a2 () (Array Int Int)
    ((as const (Array Int Int)) 0))
    
  • 取出值:(select a i)

    a-数组;i-下标;返回:a数组下标对应值
  • 存入值:(store a i v)

    a-数组;i-下标;v-新值;返回:数组本身

例子:

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const a3 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)

输出:

sat
(model
  (define-fun y () Int
    0)
  (define-fun a1 () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 0 0))
  (define-fun x () Int
    0)
  (define-fun z () Int
    0)
  (define-fun a2 () (Array Int Int)
    ((as const (Array Int Int)) 0))
  (define-fun a3 () (Array Int Int)
    ((as const (Array Int Int)) 0))
)

常数数组

当数组中每个索引都指向同一个值就变成了常数数组。可以使用as const (Array T1 T2)结构构造一个常数数组,该结构会返回指定类型的数组。原文档对这块的介绍不是很详细,我提取了主要的语句结构如下:

(declare-const a (Array Int Int))
(assert (= a ((as const (Array Int Int)) 1)))

第一句声明一个数组,第二句用断言的方式将该数组约束为常数数组。
例子:

(declare-const all1 (Array Int Int))
(declare-const a Int)
(declare-const i Int)
(assert (= all1 ((as const (Array Int Int)) 1)))
(assert (= a (select all1 i)))
(check-sat)
(get-model)
(assert (not (= a 1)))
(check-sat)

输出:

sat
(model
  (define-fun a () Int
    1)
  (define-fun all1 () (Array Int Int)
    ((as const (Array Int Int)) 1))
  (define-fun i () Int
    0)
)
unsat