时间从来不语，却回答了很多问题

post @ 2021-11-22

CTF逆向碰到几次用到z3求解器的题，如果算法便于表达式描述的话，可以直接使用z3求解，另外一般这种题都是很多位运算与循环的结合算法。例如des等。

github文档：Z3Prover/doc: Documentation (github.com)

z3库名为z3_solver，安装使用：

1	pip install z3_solver

或者下载whl包(包含中文简单使用文档)：

z3_whl.zip 下载

# coding : utf-8

from z3 import *


x = Int('x')  #声明未知数，类型是整数类型Int
y = Int('y')
solve(x > 2, y < 10, x + 2 * y == 7)
# 输出 [y = 0, x = 7]

# =================================================================================================

# 声明整数
x = Int('x')
# 声明实数
x = Real('x')
# 声明布尔类型
x = Bool('x')
# ...
x = BitVec('x', 8)
# 批量声明未知数加s

# =================================================================================================

# 更改类型
# IntVal() # 返回Z3整数
# RealVal() # 返回Z3实数
# RatVal() # 返回Z3有理数值

# =================================================================================================

# 函数化简
simplify(x + y + 2 * x + 3)
# 3 + 3*x + y

simplify(x < y + x + 2)
# Not(y <= -2)

simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))
# And(x >= 2, 2*x**2 + y**2 >= 3)


simplify((x + 1)*(y + 1), som=True) # sum-of-monomials： 单项式的和
# 1 + x + y + x*y

t = simplify((x + y)**3, som=True)
print(t)
# x*x*x + 3*x*x*y + 3*x*y*y + y*y*y


'''
simplify( <表达式> )  #对表达式进行化简
simplify( <表达式>, som=True)   #sum-of-monomials： 单项式的和 将表达式转成单项式的和
simplify( <表达式>, mul_to_power=True)   # mul_to_power 将乘法转换为乘方
'''


Q(1, 3) # 返回有理数 a/b
# 1/3


set_param() # 函数配置全局变量

# >>> solve(x**2 + y**2 == 3, x**3 == 2)
# [x = 1.2599210498?, y = -1.1885280594?]

set_param(precision=30)   #保留30位的小数

# >>> solve(x**2 + y**2 == 3, x**3 == 2)
# [x = 1.259921049894873164767210607278?, y = -1.188528059421316533710369365015?]

set_param(rational_to_decimal=True) # 以十进制形式表示有理数


'''
>>> from z3 import *
>>> x = Int('x')
>>> y = Int('y')
>>> s = Solver()
#创造一个通用solver
>>> type(s)
# Solver 类
<class ' Z3. z3. Solver'>

>>> s.add(x>10,y==x+2)  #添加约束到solver 中
>>> s
[x>10,y==x+2]
>>> s.check()   #检查solver中的约束 是否满足
sat   # satisfiable/满足

>>> s. push( )   #创建一个回溯点，即将当前栈的大小保存下来

>>> s.add(y < 11)
>>> s
[x>10,y==x+2，y<11]

>>> s.check()
unsat   # unsatisfiable/不满足

>>> s. pop(num=1)   #回溯num个点
>>> s
[x>10，y==X+2]
>>> s. check()
sat

>>> for C in s.assertions():
# assertions() 返回一个包含所有约束的AstVector

>>> s. statistics( )
# statistics() 返回最后一个check() 的统计信息
(   :max- memory     6.26
    :memory          4.37
    :mk -bool -var   1
    :num- al locs   331960806
    :rlimit-count 7016)
>>> m = s.model( )   # model() 返回最后一个check() 的model
>>> type(m)   # ModelRef 类
<class ' Z3. z3. ModelRef '>
>>> m
[x=11,y=13]
>>> for d in m.dec1s():   # decls()返回model包含了所有符号的列表
print("%S = %S" % (d.name()，m[d]))
x=11
y=13
'''
'''
Z3约束器使用流程

创建变量
例:
x = Int('x')
y = Int('y')

创建solver求解器
例：s = Solver()

添加约束条件
例：s.add(x+y==10)

检查solver中的约束是否满足
例：s.check()

利用model()输出运算结果
例：s.model()
'''

阅读此文

抓包实现易校园每日自动打卡

post @ 2021-11-22

2022-10-07 更新：大概两三个月前易校园改了接口，更简单了，我们只需抓包https://h5.xiaofubao.com/marketing/health/doDetail接口即可，脚本如下：

# POST https://h5.xiaofubao.com/marketing/health/doDetail HTTP/1.1",

h = {
    # your headers.
}

d = {
    # These are your POST data.
    # ...
    # Delete time & date infomation.
    # "createTime": "",
    # "createDate": "",
    # "updateTime": "",
    # ...
}

import requests
from pprint import pformat
requests.packages.urllib3.disable_warnings()
import yagmail

def eMail(email_to, email_title, email_content):
    # 邮件用户
    mail_user = 'your-email'
    # 授权码
    mail_key = 'your-email-key'
    # smtp服务器
    mail_host = 'your-email-smtp-server'
    try:
        mail_server = yagmail.SMTP(
            user=mail_user, password=mail_key, host=mail_host)
        mail_server.send(email_to, email_title,
                         email_content, attachments=None)
        mail_server.close()
        return True
    except Exception as e:
        print(e)
        return False


response = requests.post("https://h5.xiaofubao.com/marketing/health/doDetail", headers=h, data=d, verify=False)
pdata = pformat(response.json(), indent=4)
print(pdata)
title = ''
if response.json()['success'] == True:
    title ='打卡成功'
else:
    title = '打卡失败'
eMail('your-email', title, pdata)

每天自动打卡，有点烦了，搜索一番，加上解决了一些问题，现拿出此成熟方案。

安装fiddler4

以前高中用fiddler4，现在新版本不知道为啥变得不会用了，貌似还要交钱了，所以不太推荐。推荐下载老版本fiddler4。请自行搜索，此处不提供下载。

设置fiddler并配置证书

易校园采用https通信，因此需要配置证书。这里先进行软件的设置。安装软件后打开设置：

阅读此文

路由器运行dogcom实现一连多

post @ 2021-11-22

使用方法

某些学校使用哆点认证，dogcom可以作为该认证的客户端。它使用c编写，使用心跳包维持与认证服务器的连接。并且非常轻量，编译完后只有几十kb。这里我们简单介绍。

github项目地址：mchome/dogcom: Drcom-generic implementation in C. (github.com)

运行命令：

一般我们使用如下命令：

1	./dogcom -m dhcp -c ./drcon.conf -e -v

阅读此文

volatility内存取证

post @ 2021-11-21

$ 1_introduction

Volatility是一款非常强大的内存取证工具,它是由来自全世界的数百位知名安全专家合作开发的一套工具，可以用于windows，linux，mac osx，android等系统内存取证。Volatility是一款开源内存取证框架，能够对导出的内存镜像进行分析，通过获取内核数据结构，使用插件获取内存的详细情况以及系统的运行状态。

在不同系统下都有不同的软件版本，官网地址：https://www.volatilityfoundation.org/

官方手册：Command Reference · volatilityfoundation/volatility Wiki (github.com)

$ 2_使用

输出信息

1	volatility -f easy_dump.img imageinfo

阅读此文

brainfuck详解

post @ 2021-09-21

最近长城杯的杂项涉及到brainfuck，学习记录一下。

brainfuck被称为最小的图灵完备语言。

wiki百科

图灵完备性(Turing completness)

在可计算性理论(computability theory)中，图灵等价指的是：对于两个计算机A和B，如果A可以模拟B，B可以模拟A，就称他们是图灵等价的。

根据“丘奇-图灵”理论，图灵机是表达能力最强大的计算系统，对现实世界中的任何计算机，都可以用图灵机来模拟它。腻不腻害！

阅读此文

21羊城杯

post @ 2021-09-20

crypto_ringringring

给了个nc连接，连上后给出了一个str拼接几个字符再md5后的前五位：

数据量较小于是可以爆破：

def md5Col(one, two):
    for i in range(1048576):
        text = hex(i).replace('0x', '')
        if md5(text + one)[0:5] == two:
            print(md5(text + one))
            return text