https://github.com/satos---jp/fstar-tips で書き直し中
- まずは https://www.fstar-lang.org/tutorial/ を読む。(6章あたりまで読むと、ある程度証明付きで書くことができるようになる)
- 困った時は https://github.com/FStarLang/FStar/wiki を調べる
h = 6 | |
w = 9 | |
bo = """ | |
#####G### | |
#G # ## | |
X X | |
X X | |
## X |
import re | |
class PerfData: | |
def __init__(self): | |
self.data = {} | |
self.duration = None | |
def time(self,fn): | |
return self.data[fn] * self.duration | |
from PIL import Image | |
from PIL import ImageDraw | |
from PIL import ImageFont | |
import onnx,onnxruntime | |
from onnx import helper | |
import numpy | |
import string | |
model = onnx.load('problem.onnx','rb') |
# First, compile compiler_exploit.x with the following command. | |
# `python3 interpreter.py compiler.x < compiler_exploit.x > tmp.s` | |
# Then, run this script, and you get "exploit.s", which is an answer for this problem. | |
s = open('tmp.s').read() | |
head = s[:s.index('[123,456,789]')] | |
tail = s[s.index('[314,159,265]')+len('[314,159,265]'):] | |
headstr = ''.join(str(list(map(lambda x: ord(x),head))).split(' ')) | |
tailstr = ''.join(str(list(map(lambda x: ord(x),tail))).split(' ')) |
# gdb -q reversing -x solver.py | |
def get_byte_at(s): | |
res = gdb.execute('x/b %s' % s,to_string=True) | |
res = int(res.split('\t')[-1][2:],16) | |
return res | |
xs = [] | |
ys = [] | |
gdb.execute('b* reverse+52') |
s = """ | |
push rbx | |
sub rsp, 20h | |
mov ecx, 108h ; unsigned __int64 | |
call ??2@YAPEAX_K@Z ; operator new(unsigned __int64) | |
mov r8d, 10h ; Count | |
mov [rsp+28h+arg_0], rax | |
lea rdx, Source ; "Federation ship" | |
mov rcx, rax ; Dest | |
mov rbx, rax |
from Crypto.Cipher import AES | |
import hashlib | |
dnonce = b"531d8592bbf347cec586a5797f99da00"[:-2] | |
nonce = ("0" * len(dnonce)) | |
nonce = bytes.fromhex(nonce) | |
B = b'0' | |
key = hashlib.sha256(B).digest() |
from cryptosystem import PKCS | |
from polynomials import Polynomial as P | |
from cryptosystem_edit import PKCS as PKCS_edit | |
from flag_params import flag_encrypted_password as encpass | |
cs = PKCS.importPublicKey(open('public.key').read()) |
https://github.com/satos---jp/fstar-tips で書き直し中
#include<cstdio> | |
#include<cstring> | |
#include<vector> | |
#include<queue> | |
#include<algorithm> | |
#include<cmath> | |
#include<climits> | |
#include<string> | |
#include<set> | |
#include<map> |