Tags: reverse_engineering math
Rating:
# Boxed
After analysing the binary, I noticed the binary packed with PyInstaller.
I used pyinstxtractor to extract it.
```
$ python pyinstxtractor.py boxed
```
You will get `boxed_extracted` folder.
In this folder there is .pyc files. one of them is the main file for the challenge. `main.pyc`
I used Decompyle++ tool to decompile the file and the result was:
```
pycdc main.pyc
# Source Generated with Decompyle++
# File: main.pyc (Python 3.10)
import numpy as np
import box
def main():
try:
inp = input("What's the flag? ").encode()
inp = np.array(list(inp), np.float64)
if inp.size != box.size():
print('Not even close!')
raise SystemExit
if not box.check(inp):
print('Nope!')
raise SystemExit
print('hmm... that might be the flag...')
except:
pass
if __name__ == '__main__':
main()
```
As you see our input will convert to `np.array` and there is two functions in box library `box.size()` and `box.check(inp)`, we have to check them.
In boxed_extracted I found `box` library with name `box.cpython-310-x86_64-linux-gnu.so`.
So, I opened `box.cpython-310-x86_64-linux-gnu.so` with IDA to analyse it.
I searched in the functions list with keywords `size` and `check` and found `box.size()` function return the flag size only.
```
.text:00007FF1CB1F51E0 _ZN8__main__9size_2418B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE proc near
.text:00007FF1CB1F51E0 ; CODE XREF: __pycc_method_size+3A↓p
.text:00007FF1CB1F51E0 ; cfunc__ZN8__main__9size_2418B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE+C↓p
.text:00007FF1CB1F51E0 mov qword ptr [rdi], 1Ah
.text:00007FF1CB1F51E7 retn
.text:00007FF1CB1F51E7 _ZN8__main__9size_2418B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE endp
```
The flag size is 0x1A == 26 .
In the `box.check(inp)` it should receive our input as np.array then make some calculations to find the input was correct or not.
```
.text:00007FF1CB1F4BF0 _ZN8__main__9check_241B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE5ArrayIdLi1E1A7mutable7alignedE proc near
.
.
.
.[cut]
.
.
.
.text:00007FF1CB1F4CB1 lea rbx, big_array
.text:00007FF1CB1F4CB8 lea rdi, [rsp+88h+var_68] ; int
.text:00007FF1CB1F4CBD lea rsi, [rsp+88h+var_78] ; int
.text:00007FF1CB1F4CC2 mov r8d, 1EEh ; int
.text:00007FF1CB1F4CC8 mov r9d, 8 ; int
.text:00007FF1CB1F4CCE mov edx, 0 ; int
.text:00007FF1CB1F4CD3 mov ecx, 0 ; int
.text:00007FF1CB1F4CD8 push 8
.text:00007FF1CB1F4CDA push r14 ; __int64
.text:00007FF1CB1F4CDC push rax ; x
.text:00007FF1CB1F4CDD push 8 ; int
.text:00007FF1CB1F4CDF push r14 ; int
.text:00007FF1CB1F4CE1 push 0 ; int
.text:00007FF1CB1F4CE3 push r12 ; __int64
.text:00007FF1CB1F4CE5 push 8 ; int
.text:00007FF1CB1F4CE7 push 0D0h ; int
.text:00007FF1CB1F4CEC push 1Ah ; lda
.text:00007FF1CB1F4CEE push 13h ; n
.text:00007FF1CB1F4CF0 push rbx ; a
.text:00007FF1CB1F4CF1 call _ZN5numba2np6linalg8dot_2_mv12_3clocals_3e13dot_impl_2412B44c8tJTC_2fWQA9HW1CcAv0EjzIkAdRogEkUlYBZmgA_3dE5ArrayIdLi2E1C8readonly7alignedE5ArrayIdLi1E1C7mutable7alignedE ; numba::np::linalg::dot_2_mv::_3clocals_3e::dot_impl_2412(Array<double,2,C,readonly,aligned>,Array<double,1,C,mutable,aligned>)
.text:00007FF1CB1F4CF6 add rsp, 60h
.
.
.
.[cut]
.
.
.
.text:00007FF1CB1F4D61 lea r8, final_array
.text:00007FF1CB1F4D68 cmp rsi, r8
.text:00007FF1CB1F4D6B setnbe dil
.text:00007FF1CB1F4D6F xor esi, esi
.text:00007FF1CB1F4D71 test r9b, r10b
.text:00007FF1CB1F4D74 jnz loc_7FF1CB1F4E5E
.text:00007FF1CB1F4D7A and dl, dil
.text:00007FF1CB1F4D7D jnz loc_7FF1CB1F4E5E
.text:00007FF1CB1F4D83 movupd xmm0, xmmword ptr [r14]
.text:00007FF1CB1F4D88 movupd xmm5, xmmword ptr [r14+10h]
.text:00007FF1CB1F4D8E movupd xmm1, xmmword ptr [r14+20h]
.text:00007FF1CB1F4D94 movupd xmm7, xmmword ptr [r14+30h]
.text:00007FF1CB1F4D9A movupd xmm2, xmmword ptr [r14+40h]
.text:00007FF1CB1F4DA0 movupd xmm6, xmmword ptr [r14+50h]
.text:00007FF1CB1F4DA6 movupd xmm3, xmmword ptr [r14+60h]
.text:00007FF1CB1F4DAC movupd xmm4, xmmword ptr [r14+70h]
.text:00007FF1CB1F4DB2 cmpeqpd xmm5, xmmword ptr cs:qword_7FF1CB208000
.text:00007FF1CB1F4DBB cmpeqpd xmm0, xmmword ptr cs:qword_7FF1CB208000+10h
.
.
.
.[cut]
.
.
.
.text:00007FF1CB1F4F24 _ZN8__main__9check_241B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE5ArrayIdLi1E1A7mutable7alignedE endp
```
I noticed the library use numba function `dot_2_mv` to multiply the input_array with a big_array
and comparing the result with the final_array.
After googleing I found `dot_2_mv` is equivelant to `numpy.dot`.
So, I decided to extract the data in the big_array and final_array.
The big_array was with 494 items and because the input_array type was np.float64, I jumped to the big_array address and convert it's data to float64.
and this is the result
```
.rodata:00007FF1CB208118 ; double big_array[494]
.rodata:00007FF1CB208118 big_array dq 160.0, 477.0, 197.0, 699.0, 883.0, 300.0, 799.0, 113.0, 159.0, 288.0, 833.0, 489.0, 782.0, 895.0, 603.0, 723.0, 327.0, 129.0, 622.0
.rodata:00007FF1CB208118 dq 376.0, 664.0, 487.0, 841.0, 512.0, 382.0, 625.0, 656.0, 813.0, 329.0, 934.0, 650.0, 559.0, 421.0, 769.0, 345.0, 666.0, 107.0, 779.0
.rodata:00007FF1CB208118 dq 948.0, 141.0, 126.0, 958.0, 647.0, 576.0, 252.0, 297.0, 418.0, 602.0, 800.0, 174.0, 532.0, 287.0, 172.0, 411.0, 516.0, 780.0, 104.0
.rodata:00007FF1CB208118 dq 669.0, 524.0, 696.0, 735.0, 754.0, 654.0, 947.0, 982.0, 195.0, 453.0, 260.0, 860.0, 401.0, 132.0, 262.0, 506.0, 895.0, 297.0, 529.0
.rodata:00007FF1CB208118 dq 961.0, 689.0, 343.0, 881.0, 679.0, 350.0, 877.0, 514.0, 915.0, 323.0, 863.0, 583.0, 622.0, 748.0, 886.0, 934.0, 575.0, 202.0, 843.0
.rodata:00007FF1CB208118 dq 691.0, 809.0, 480.0, 119.0, 155.0, 655.0, 289.0, 740.0, 543.0, 566.0, 191.0, 639.0, 444.0, 855.0, 363.0, 963.0, 797.0, 613.0, 720.0
.rodata:00007FF1CB208118 dq 307.0, 890.0, 475.0, 730.0, 765.0, 274.0, 344.0, 751.0, 504.0, 623.0, 961.0, 880.0, 747.0, 129.0, 262.0, 457.0, 593.0, 480.0, 156.0
.rodata:00007FF1CB208118 dq 987.0, 719.0, 115.0, 533.0, 760.0, 108.0, 747.0, 880.0, 726.0, 474.0, 749.0, 874.0, 475.0, 735.0, 435.0, 421.0, 126.0, 270.0, 949.0
.rodata:00007FF1CB208118 dq 311.0, 359.0, 398.0, 514.0, 299.0, 473.0, 542.0, 656.0, 279.0, 793.0, 618.0, 707.0, 504.0, 356.0, 920.0, 432.0, 605.0, 917.0, 410.0
.rodata:00007FF1CB208118 dq 233.0, 772.0, 989.0, 892.0, 107.0, 179.0, 335.0, 737.0, 636.0, 392.0, 453.0, 791.0, 420.0, 553.0, 949.0, 834.0, 669.0, 690.0, 692.0
.rodata:00007FF1CB208118 dq 824.0, 564.0, 461.0, 966.0, 422.0, 589.0, 359.0, 599.0, 285.0, 949.0, 703.0, 263.0, 608.0, 772.0, 871.0, 890.0, 143.0, 237.0, 944.0
.rodata:00007FF1CB208118 dq 728.0, 682.0, 798.0, 929.0, 833.0, 737.0, 407.0, 210.0, 347.0, 703.0, 546.0, 710.0, 481.0, 919.0, 986.0, 204.0, 818.0, 611.0, 144.0
.rodata:00007FF1CB208118 dq 908.0, 643.0, 802.0, 612.0, 565.0, 746.0, 609.0, 803.0, 343.0, 833.0, 214.0, 923.0, 592.0, 186.0, 191.0, 837.0, 476.0, 155.0, 289.0
.rodata:00007FF1CB208118 dq 406.0, 267.0, 615.0, 532.0, 337.0, 576.0, 706.0, 902.0, 778.0, 857.0, 867.0, 649.0, 449.0, 833.0, 803.0, 839.0, 892.0, 902.0, 430.0
.rodata:00007FF1CB208118 dq 584.0, 842.0, 160.0, 247.0, 982.0, 765.0, 634.0, 302.0, 554.0, 896.0, 269.0, 391.0, 908.0, 749.0, 500.0, 728.0, 854.0, 279.0, 654.0
.rodata:00007FF1CB208118 dq 814.0, 232.0, 403.0, 245.0, 976.0, 163.0, 764.0, 463.0, 911.0, 533.0, 685.0, 124.0, 716.0, 441.0, 931.0, 427.0, 882.0, 224.0, 892.0
.rodata:00007FF1CB208118 dq 141.0, 563.0, 760.0, 841.0, 604.0, 605.0, 635.0, 740.0, 874.0, 382.0, 149.0, 376.0, 613.0, 137.0, 932.0, 186.0, 742.0, 921.0, 697.0
.rodata:00007FF1CB208118 dq 574.0, 863.0, 230.0, 103.0, 281.0, 464.0, 553.0, 169.0, 807.0, 390.0, 617.0, 936.0, 999.0, 189.0, 882.0, 439.0, 385.0, 335.0, 306.0
.rodata:00007FF1CB208118 dq 248.0, 189.0, 506.0, 738.0, 873.0, 935.0, 261.0, 355.0, 670.0, 208.0, 984.0, 669.0, 845.0, 704.0, 744.0, 902.0, 895.0, 401.0, 173.0
.rodata:00007FF1CB208118 dq 132.0, 977.0, 921.0, 710.0, 805.0, 697.0, 545.0, 423.0, 694.0, 377.0, 247.0, 195.0, 667.0, 905.0, 191.0, 355.0, 180.0, 433.0, 952.0
.rodata:00007FF1CB208118 dq 353.0, 825.0, 650.0, 739.0, 295.0, 653.0, 743.0, 986.0, 650.0, 385.0, 690.0, 408.0, 225.0, 656.0, 831.0, 851.0, 412.0, 623.0, 937.0
.rodata:00007FF1CB208118 dq 677.0, 735.0, 504.0, 167.0, 994.0, 654.0, 101.0, 991.0, 296.0, 390.0, 285.0, 784.0, 857.0, 219.0, 722.0, 880.0, 424.0, 463.0, 827.0
.rodata:00007FF1CB208118 dq 806.0, 345.0, 511.0, 146.0, 307.0, 498.0, 962.0, 533.0, 857.0, 641.0, 720.0, 613.0, 836.0, 770.0, 583.0, 319.0, 382.0, 575.0, 809.0
.rodata:00007FF1CB208118 dq 515.0, 466.0, 231.0, 784.0, 815.0, 109.0, 148.0, 908.0, 572.0, 241.0, 159.0, 810.0, 495.0, 405.0, 645.0, 899.0, 645.0, 891.0, 350.0
.rodata:00007FF1CB208118 dq 385.0, 480.0, 155.0, 379.0, 501.0, 454.0, 416.0, 848.0, 358.0, 402.0, 424.0, 477.0, 859.0, 854.0, 752.0, 492.0, 790.0, 201.0, 227.0
.rodata:00007FF1CB208118 dq 973.0, 312.0, 567.0, 459.0, 239.0, 449.0, 422.0, 948.0, 119.0, 261.0, 787.0, 925.0, 181.0, 310.0, 918.0, 766.0, 727.0, 175.0, 809.0
```
Also the final_array was 19 items, and convert it to float64.
```
.rodata:00007FF1CB209088 ; double final_array[19]
.rodata:00007FF1CB209088 final_array dq 1256330.0, 1339998.0, 1346424.0, 1447434.0, 1500836.0
.rodata:00007FF1CB209088 dq 1343196.0, 1341708.0, 1585556.0, 1653047.0, 1365749.0
.rodata:00007FF1CB209088 dq 1648449.0, 1500874.0, 1335251.0, 1379725.0, 1399574.0
.rodata:00007FF1CB209088 dq 1467166.0, 1487079.0, 1178725.0, 1419771.0
```
Now, here is our arguments size:
flag_array: 26
big_array: 494
final_array: 19
To solve this math puzzle, we need to reshape the big_array to be in 2D-dimension (19x26) and also need to get the inverse array of the big_array.
I programmed a small python script to achive that but unfortunatly the result wasn't correct.
```
import numpy as np
final_array = np.array([
1256330.0, 1339998.0, 1346424.0, 1447434.0,
1500836.0, 1343196.0, 1341708.0, 1585556.0,
1653047.0, 1365749.0, 1648449.0, 1500874.0,
1335251.0, 1379725.0, 1399574.0, 1467166.0,
1487079.0, 1178725.0, 1419771.0], np.float64)
big_array = np.array([
[160.0, 477.0, 197.0, 699.0, 883.0, 300.0, 799.0, 113.0, 159.0, 288.0, 833.0, 489.0, 782.0, 895.0, 603.0, 723.0, 327.0, 129.0, 622.0],
[376.0, 664.0, 487.0, 841.0, 512.0, 382.0, 625.0, 656.0, 813.0, 329.0, 934.0, 650.0, 559.0, 421.0, 769.0, 345.0, 666.0, 107.0, 779.0],
[948.0, 141.0, 126.0, 958.0, 647.0, 576.0, 252.0, 297.0, 418.0, 602.0, 800.0, 174.0, 532.0, 287.0, 172.0, 411.0, 516.0, 780.0, 104.0],
[669.0, 524.0, 696.0, 735.0, 754.0, 654.0, 947.0, 982.0, 195.0, 453.0, 260.0, 860.0, 401.0, 132.0, 262.0, 506.0, 895.0, 297.0, 529.0],
[961.0, 689.0, 343.0, 881.0, 679.0, 350.0, 877.0, 514.0, 915.0, 323.0, 863.0, 583.0, 622.0, 748.0, 886.0, 934.0, 575.0, 202.0, 843.0],
[691.0, 809.0, 480.0, 119.0, 155.0, 655.0, 289.0, 740.0, 543.0, 566.0, 191.0, 639.0, 444.0, 855.0, 363.0, 963.0, 797.0, 613.0, 720.0],
[307.0, 890.0, 475.0, 730.0, 765.0, 274.0, 344.0, 751.0, 504.0, 623.0, 961.0, 880.0, 747.0, 129.0, 262.0, 457.0, 593.0, 480.0, 156.0],
[987.0, 719.0, 115.0, 533.0, 760.0, 108.0, 747.0, 880.0, 726.0, 474.0, 749.0, 874.0, 475.0, 735.0, 435.0, 421.0, 126.0, 270.0, 949.0],
[311.0, 359.0, 398.0, 514.0, 299.0, 473.0, 542.0, 656.0, 279.0, 793.0, 618.0, 707.0, 504.0, 356.0, 920.0, 432.0, 605.0, 917.0, 410.0],
[233.0, 772.0, 989.0, 892.0, 107.0, 179.0, 335.0, 737.0, 636.0, 392.0, 453.0, 791.0, 420.0, 553.0, 949.0, 834.0, 669.0, 690.0, 692.0],
[824.0, 564.0, 461.0, 966.0, 422.0, 589.0, 359.0, 599.0, 285.0, 949.0, 703.0, 263.0, 608.0, 772.0, 871.0, 890.0, 143.0, 237.0, 944.0],
[728.0, 682.0, 798.0, 929.0, 833.0, 737.0, 407.0, 210.0, 347.0, 703.0, 546.0, 710.0, 481.0, 919.0, 986.0, 204.0, 818.0, 611.0, 144.0],
[908.0, 643.0, 802.0, 612.0, 565.0, 746.0, 609.0, 803.0, 343.0, 833.0, 214.0, 923.0, 592.0, 186.0, 191.0, 837.0, 476.0, 155.0, 289.0],
[406.0, 267.0, 615.0, 532.0, 337.0, 576.0, 706.0, 902.0, 778.0, 857.0, 867.0, 649.0, 449.0, 833.0, 803.0, 839.0, 892.0, 902.0, 430.0],
[584.0, 842.0, 160.0, 247.0, 982.0, 765.0, 634.0, 302.0, 554.0, 896.0, 269.0, 391.0, 908.0, 749.0, 500.0, 728.0, 854.0, 279.0, 654.0],
[814.0, 232.0, 403.0, 245.0, 976.0, 163.0, 764.0, 463.0, 911.0, 533.0, 685.0, 124.0, 716.0, 441.0, 931.0, 427.0, 882.0, 224.0, 892.0],
[141.0, 563.0, 760.0, 841.0, 604.0, 605.0, 635.0, 740.0, 874.0, 382.0, 149.0, 376.0, 613.0, 137.0, 932.0, 186.0, 742.0, 921.0, 697.0],
[574.0, 863.0, 230.0, 103.0, 281.0, 464.0, 553.0, 169.0, 807.0, 390.0, 617.0, 936.0, 999.0, 189.0, 882.0, 439.0, 385.0, 335.0, 306.0],
[248.0, 189.0, 506.0, 738.0, 873.0, 935.0, 261.0, 355.0, 670.0, 208.0, 984.0, 669.0, 845.0, 704.0, 744.0, 902.0, 895.0, 401.0, 173.0],
[132.0, 977.0, 921.0, 710.0, 805.0, 697.0, 545.0, 423.0, 694.0, 377.0, 247.0, 195.0, 667.0, 905.0, 191.0, 355.0, 180.0, 433.0, 952.0],
[353.0, 825.0, 650.0, 739.0, 295.0, 653.0, 743.0, 986.0, 650.0, 385.0, 690.0, 408.0, 225.0, 656.0, 831.0, 851.0, 412.0, 623.0, 937.0],
[677.0, 735.0, 504.0, 167.0, 994.0, 654.0, 101.0, 991.0, 296.0, 390.0, 285.0, 784.0, 857.0, 219.0, 722.0, 880.0, 424.0, 463.0, 827.0],
[806.0, 345.0, 511.0, 146.0, 307.0, 498.0, 962.0, 533.0, 857.0, 641.0, 720.0, 613.0, 836.0, 770.0, 583.0, 319.0, 382.0, 575.0, 809.0],
[515.0, 466.0, 231.0, 784.0, 815.0, 109.0, 148.0, 908.0, 572.0, 241.0, 159.0, 810.0, 495.0, 405.0, 645.0, 899.0, 645.0, 891.0, 350.0],
[385.0, 480.0, 155.0, 379.0, 501.0, 454.0, 416.0, 848.0, 358.0, 402.0, 424.0, 477.0, 859.0, 854.0, 752.0, 492.0, 790.0, 201.0, 227.0],
[973.0, 312.0, 567.0, 459.0, 239.0, 449.0, 422.0, 948.0, 119.0, 261.0, 787.0, 925.0, 181.0, 310.0, 918.0, 766.0, 727.0, 175.0, 809.0]], np.float64)
big_array = big_array.reshape(19, 26)
# big_array_inv = np.linalg.inv(big_array) # it raise error because the big_array is not a squared array.
big_array_inv = np.linalg.pinv(big_array)
result = big_array_inv.dot(final_array)
result = result.astype(int)
print(''.join([chr(c) for c in result]))
```
The result: `|nbh\XD}hMbx-ySl5t2dintESp`
WHY !!!!
After googleing I figured out that the big_array is not a squared array,
and for this reason I can't use `np.linalg.inv` and instead I used `np.linalg.pinv`
and because the function `np.linalg.pinv` return the nearest inverse for the target matrix, the result was not correct.
At this moment I decided to use z3 Solver and here is my final python script:
```
import numpy as np
from z3 import Solver, BitVec, sat
a = np.array([
1256330.0, 1339998.0, 1346424.0, 1447434.0,
1500836.0, 1343196.0, 1341708.0, 1585556.0,
1653047.0, 1365749.0, 1648449.0, 1500874.0,
1335251.0, 1379725.0, 1399574.0, 1467166.0,
1487079.0, 1178725.0, 1419771.0], np.float64)
b = np.array([
[160.0, 477.0, 197.0, 699.0, 883.0, 300.0, 799.0, 113.0, 159.0, 288.0, 833.0, 489.0, 782.0, 895.0, 603.0, 723.0, 327.0, 129.0, 622.0],
[376.0, 664.0, 487.0, 841.0, 512.0, 382.0, 625.0, 656.0, 813.0, 329.0, 934.0, 650.0, 559.0, 421.0, 769.0, 345.0, 666.0, 107.0, 779.0],
[948.0, 141.0, 126.0, 958.0, 647.0, 576.0, 252.0, 297.0, 418.0, 602.0, 800.0, 174.0, 532.0, 287.0, 172.0, 411.0, 516.0, 780.0, 104.0],
[669.0, 524.0, 696.0, 735.0, 754.0, 654.0, 947.0, 982.0, 195.0, 453.0, 260.0, 860.0, 401.0, 132.0, 262.0, 506.0, 895.0, 297.0, 529.0],
[961.0, 689.0, 343.0, 881.0, 679.0, 350.0, 877.0, 514.0, 915.0, 323.0, 863.0, 583.0, 622.0, 748.0, 886.0, 934.0, 575.0, 202.0, 843.0],
[691.0, 809.0, 480.0, 119.0, 155.0, 655.0, 289.0, 740.0, 543.0, 566.0, 191.0, 639.0, 444.0, 855.0, 363.0, 963.0, 797.0, 613.0, 720.0],
[307.0, 890.0, 475.0, 730.0, 765.0, 274.0, 344.0, 751.0, 504.0, 623.0, 961.0, 880.0, 747.0, 129.0, 262.0, 457.0, 593.0, 480.0, 156.0],
[987.0, 719.0, 115.0, 533.0, 760.0, 108.0, 747.0, 880.0, 726.0, 474.0, 749.0, 874.0, 475.0, 735.0, 435.0, 421.0, 126.0, 270.0, 949.0],
[311.0, 359.0, 398.0, 514.0, 299.0, 473.0, 542.0, 656.0, 279.0, 793.0, 618.0, 707.0, 504.0, 356.0, 920.0, 432.0, 605.0, 917.0, 410.0],
[233.0, 772.0, 989.0, 892.0, 107.0, 179.0, 335.0, 737.0, 636.0, 392.0, 453.0, 791.0, 420.0, 553.0, 949.0, 834.0, 669.0, 690.0, 692.0],
[824.0, 564.0, 461.0, 966.0, 422.0, 589.0, 359.0, 599.0, 285.0, 949.0, 703.0, 263.0, 608.0, 772.0, 871.0, 890.0, 143.0, 237.0, 944.0],
[728.0, 682.0, 798.0, 929.0, 833.0, 737.0, 407.0, 210.0, 347.0, 703.0, 546.0, 710.0, 481.0, 919.0, 986.0, 204.0, 818.0, 611.0, 144.0],
[908.0, 643.0, 802.0, 612.0, 565.0, 746.0, 609.0, 803.0, 343.0, 833.0, 214.0, 923.0, 592.0, 186.0, 191.0, 837.0, 476.0, 155.0, 289.0],
[406.0, 267.0, 615.0, 532.0, 337.0, 576.0, 706.0, 902.0, 778.0, 857.0, 867.0, 649.0, 449.0, 833.0, 803.0, 839.0, 892.0, 902.0, 430.0],
[584.0, 842.0, 160.0, 247.0, 982.0, 765.0, 634.0, 302.0, 554.0, 896.0, 269.0, 391.0, 908.0, 749.0, 500.0, 728.0, 854.0, 279.0, 654.0],
[814.0, 232.0, 403.0, 245.0, 976.0, 163.0, 764.0, 463.0, 911.0, 533.0, 685.0, 124.0, 716.0, 441.0, 931.0, 427.0, 882.0, 224.0, 892.0],
[141.0, 563.0, 760.0, 841.0, 604.0, 605.0, 635.0, 740.0, 874.0, 382.0, 149.0, 376.0, 613.0, 137.0, 932.0, 186.0, 742.0, 921.0, 697.0],
[574.0, 863.0, 230.0, 103.0, 281.0, 464.0, 553.0, 169.0, 807.0, 390.0, 617.0, 936.0, 999.0, 189.0, 882.0, 439.0, 385.0, 335.0, 306.0],
[248.0, 189.0, 506.0, 738.0, 873.0, 935.0, 261.0, 355.0, 670.0, 208.0, 984.0, 669.0, 845.0, 704.0, 744.0, 902.0, 895.0, 401.0, 173.0],
[132.0, 977.0, 921.0, 710.0, 805.0, 697.0, 545.0, 423.0, 694.0, 377.0, 247.0, 195.0, 667.0, 905.0, 191.0, 355.0, 180.0, 433.0, 952.0],
[353.0, 825.0, 650.0, 739.0, 295.0, 653.0, 743.0, 986.0, 650.0, 385.0, 690.0, 408.0, 225.0, 656.0, 831.0, 851.0, 412.0, 623.0, 937.0],
[677.0, 735.0, 504.0, 167.0, 994.0, 654.0, 101.0, 991.0, 296.0, 390.0, 285.0, 784.0, 857.0, 219.0, 722.0, 880.0, 424.0, 463.0, 827.0],
[806.0, 345.0, 511.0, 146.0, 307.0, 498.0, 962.0, 533.0, 857.0, 641.0, 720.0, 613.0, 836.0, 770.0, 583.0, 319.0, 382.0, 575.0, 809.0],
[515.0, 466.0, 231.0, 784.0, 815.0, 109.0, 148.0, 908.0, 572.0, 241.0, 159.0, 810.0, 495.0, 405.0, 645.0, 899.0, 645.0, 891.0, 350.0],
[385.0, 480.0, 155.0, 379.0, 501.0, 454.0, 416.0, 848.0, 358.0, 402.0, 424.0, 477.0, 859.0, 854.0, 752.0, 492.0, 790.0, 201.0, 227.0],
[973.0, 312.0, 567.0, 459.0, 239.0, 449.0, 422.0, 948.0, 119.0, 261.0, 787.0, 925.0, 181.0, 310.0, 918.0, 766.0, 727.0, 175.0, 809.0]]], np.float64)
f = []
sol = Solver()
for i in range(26):
f.append(BitVec('f%2d' % i, 32))
if i not in [0, 1, 2, 3, 4, 5, 25]:
sol.add(f[i] > 0x2f, f[i] < 0x7b)
for j in range(0x3a, 0x41): # exclude chars
sol.add(f[i] != j)
# add the characters I know in the flag
sol.add(f[0] == ord('t'))
sol.add(f[1] == ord('j'))
sol.add(f[2] == ord('c'))
sol.add(f[3] == ord('t'))
sol.add(f[4] == ord('f'))
sol.add(f[5] == ord('{'))
sol.add(f[25] == ord('}'))
b = b.reshape(19, 26)
a = list(map(int, a)) # convert float values to integer for final_array
for j in range(19):
c = b[j,:] # get a row values
c = list(map(int, c)) # convert float values to integer
sum1 = 0
for i in range(26):
sum1 += c[i] * f[i]
sol.add(sum1 == a[j])
# https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation/70656700#70656700
def all_smt(s, initial_terms):
def block_term(s, m, t):
s.add(t != m.eval(t, model_completion=True))
def fix_term(s, m, t):
s.add(t == m.eval(t, model_completion=True))
def all_smt_rec(terms):
if sat == s.check():
m = s.model()
yield m
for i in range(len(terms)):
s.push()
block_term(s, m, terms[i])
for j in range(i):
fix_term(s, m, terms[j])
yield from all_smt_rec(terms[i:])
s.pop()
yield from all_smt_rec(list(initial_terms))
for m in all_smt(sol, f):
flag = ''
for i in f:
flag += chr(m[i].as_long())
print(flag)
exit()
```
Here is the flag: `tjctf{1ts_ju5t_l1n3s_lm40}`
