3
리버스 엔지니어링 연습의 일환으로 아래 프로그램을 만족시키는 사용자 이름과 암호를 찾기 위해 Z3 솔버를 작성하려고합니다. 이것은 모든 사람들이 참조하는 z3py 튜토리얼 (rise4fun)이 다운 되었기 때문에 특히 어렵습니다.Z3Py에서 배열을 반복하는 방법
#include <iostream>
#include <string>
using namespace std;
int main() {
string name, pass;
cout << "Name: ";
cin >> name;
cout << "Pass: ";
cin >> pass;
int sum = 0;
for (size_t i = 0; i < name.size(); i++) {
char c = name[i];
if (c < 'A') {
cout << "Lose: char is less than A" << endl;
return 1;
}
if (c > 'Z') {
sum += c - 32;
} else {
sum += c;
}
}
int r1 = 0x5678^sum;
int r2 = 0;
for (size_t i = 0; i < pass.size(); i++) {
char c = pass[i];
c -= 48;
r2 *= 10;
r2 += c;
}
r2 ^= 0x1234;
cout << "r1: " << r1 << endl;
cout << "r2: " << r2 << endl;
if (r1 == r2) {
cout << "Win" << endl;
} else {
cout << "Lose: r1 and r2 don't match" << endl;
}
}
바이너리 어셈블리에서이 코드를 얻었습니다. 잘못되었을 수도 있지만 해결사를 작성하는 데 집중하고 싶습니다. 난 그냥 r1을 계산, 첫 번째 부분으로 시작하고,이 내가 무엇을 가지고 :
from z3 import *
s = Solver()
sum = Int('sum')
name = Array('name', IntSort(), IntSort())
for c in name:
s.add(c < 65)
if c > 90:
sum += c - 32
else:
sum += c
r1 = Xor(sum, 0x5678)
print s.check()
print s.model()
내가 주장하고있어 모든이 배열의 'A'보다 더 문자가없는, 그래서 기대입니다 숫자가 65보다 큰 모든 배열을 되 찾을 수 있습니다.
분명히 이것은 무한 루프이기 때문에 완전히 잘못되었습니다. 또한, 내가 0으로 초기화되는지 알 수 없기 때문에 나는 합계를 정확히 계산하고 있는지 확신하지 못합니다. 누군가이 첫 번째 루프를 작동시키는 방법을 파악하는 데 도움이 될 수 있습니까?
편집 :
from z3 import * s = Solver() sum = 0 name = Array('name', BitVecSort(32), BitVecSort(32)) i = Int('i') for i in xrange(0, 1): s.add(name[i] >= 65) s.add(name[i] < 127) if name[i] > 90: sum += name[i] - 32 else: sum += name[i] r1 = sum^0x5678 passwd = Array('passwd', BitVecSort(32), BitVecSort(32)) r2 = 0 for i in xrange(0, 5): s.add(passwd[i] < 127) s.add(passwd[i] >= 48) c = passwd[i] - 48 r2 *= 10 r2 += c r2 ^= 0x1234 s.add(r1 == r2) print s.check() print s.model() 이 코드
이 나에게 올바른 사용자 이름과 암호를 제공 할 수 있었다 : 내가 위의 C++ 코드에 가까운 Z3 스크립트를 얻을 수있었습니다. 그러나, 나는 사용자 이름과 패스워드를위한 길이를 하드 코드했다. 길이를 하드 코딩 할 필요가 없도록 스크립트를 어떻게 변경합니까? 그리고 프로그램을 실행할 때마다 어떻게 다른 솔루션을 생성합니까?
원래 문제는 해결할 수 있었지만 사용자 이름과 암호의 길이를 하드 코딩해야했습니다. 수량 한정자를 사용하는 방법을 알 수 없었습니다. 업데이트 된 코드를 사용하여 좀 더 구체적인 예를 들어 주시겠습니까? – gsingh2011