satos---jp

## solver.py

h = 6
w = 9

bo = """
#####G###
#G #   ##
 X     X
     X X
##     X

## port_fstar_tdiff.py
import re

class PerfData:
	def __init__(self):
		self.data = {}
		self.duration = None

	def time(self,fn):
		return self.data[fn] * self.duration


## solver.py
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')

## __generator.py
# 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(' '))

## solver.py
# 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')

## fed_data.py
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

## decode.py
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()

## remote.py
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())

## tips.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                satos---jp
                / tips.md
            
            
              Last active
              October 18, 2020 13:26
            
              
                FStar Tips
              
          
    https://github.com/satos---jp/fstar-tips で書き直し中
For fstar users

入門


まずは https://www.fstar-lang.org/tutorial/ を読む。(6章あたりまで読むと、ある程度証明付きで書くことができるようになる)
困った時は https://github.com/FStarLang/FStar/wiki を調べる

辞書的に便利なページ

https://github.com/FStarLang/FStar/wiki/F%2A-symbols-reference
https://github.com/FStarLang/FStar/wiki/Qualifiers-for-definitions-and-declarations
https://github.com/FStarLang/FStar/wiki/Pragmas-%28%23set-options%2C-%23reset-options%29


## template.cpp
#include<cstdio>
#include<cstring>
#include<vector>
#include<queue>
#include<algorithm>
#include<cmath>
#include<climits>
#include<string>
#include<set>
#include<map>
	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())
	#include<cstdio>
	#include<cstring>
	#include<vector>
	#include<queue>
	#include<algorithm>
	#include<cmath>
	#include<climits>
	#include<string>
	#include<set>
	#include<map>