# Solving Cryptography Problems Using SAT

CS 463/480 Lecture, Dr. Lawlor

There's a very general and powerful technique to solve cryptography and other hard search problems using a boolean satisfiability (SAT) solver.  My favorite interface to SAT is with C++, using CBMC (version 4.5 works the best for me, it's hard to get version 5+ to actually tell you the answer in a clear way).

The input to CBMC is a C++ program including uninitialized variables.  The output is a set of values for those variables that makes the program crash, or fail its assertion checks.  We use this to solve crypto problems by adding an assertion that there is no solution--the assertion only fails if CBMC has found a solution.

Here's how we'd use CBMC to solve a really trivial cryptosystem, xor on a single byte:
`/** Trivial demo of crypto using CBMC for a single byte. find the plaintext for an xor cipher, given known key and ciphertext.*/typedef unsigned char byte;int main() {	byte plaintext; // uninitialized (we're hoping to find this)	const byte key='K';  	const byte ciphertext=0x12; // bytes of ciphertext	// Perform the encryption here:	bool good=true;	byte out=plaintext ^ key;	if (out!=ciphertext)		good=false;	// Dare the checker to find a solution	assert(!good);	return 0;}`
This finds an assertion failure when plaintext=89 (01011001)

Multi-byte inputs are just as easy:
```/** Trivial demo of crypto using CBMC for an array of bytes: find the plaintext for an xor cipher, given known key and ciphertext.*/typedef unsigned char byte;int main() {	const int length=2;	byte plaintext[length]; // uninitialized (we're hoping to find this)	const byte key[length]={'K','E'};  // bytes of the key	const byte ciphertext[length]={0x12,0x2A}; // bytes of ciphertext	// Perform the encryption here:	bool good=true;	for (int i=0;i<length;i++)	{		byte out=plaintext[i] ^ key[i];		if (out!=ciphertext[i])			good=false;	}	// Dare the checker to find a solution
assert(!good);	return 0;}```
The powerful part is this can solve problems even when the search space is big, and the processing is more complex.

## CBMC for Real Crypto Problems

Example challenge: Another Xor, Crypto 100 at CSAW 2017 CTF
• Known ciphertext, in "encrypted": 274c10121a0100495b502d551c557f0b0833585d1b27030b5228040d3753490a1c025415051525455118001911534a0052560a14594f0b1e490a010c4514411e070014615a181b02521b580305170002074b0a1a4c414d1f1d171d00151b1d0f480e491e0249010c150050115c505850434203421354424c1150430b5e094d144957080d4444254643
• Known algorithm, in "cipher.py" (basically just byte-for-byte xor)
• Unknown key
• Unknown plaintext, although probably starts with "flag".
Step one is to write down what we know about the problem as a C++ program.  The "encrypted" data is a long string of hex, and we want to initialize a C++ array, so we do a regex find and replace to put in the C++ hex 0x prefix, and add commas so we can initialize an array:
Find: ([0-9a-f][0-9a-f])
Replace: , 0x\1

So far we have:
`/** Break crypto for 100: xor with repeating key.*/typedef unsigned char byte;int main() {	const int length=137; // == 274/2, because the "encrypted" file has 274 bytes of hex	int keylength; // unknown	const byte plaintext[length]; // unknown	const byte key[keylength]; // unknown	const byte ciphertext[length]={		0x27, 0x4c, 0x10, 0x12, 0x1a, 0x01, 0x00, 0x49, 0x5b, 0x50, 0x2d, 0x55, 0x1c, 0x55, 0x7f, 0x0b, 0x08, 0x33, 0x58, 0x5d, 0x1b, 0x27, 0x03, 0x0b, 0x52, 0x28, 0x04, 0x0d, 0x37, 0x53, 0x49, 0x0a, 0x1c, 0x02, 0x54, 0x15, 0x05, 0x15, 0x25, 0x45, 0x51, 0x18, 0x00, 0x19, 0x11, 0x53, 0x4a, 0x00, 0x52, 0x56, 0x0a, 0x14, 0x59, 0x4f, 0x0b, 0x1e, 0x49, 0x0a, 0x01, 0x0c, 0x45, 0x14, 0x41, 0x1e, 0x07, 0x00, 0x14, 0x61, 0x5a, 0x18, 0x1b, 0x02, 0x52, 0x1b, 0x58, 0x03, 0x05, 0x17, 0x00, 0x02, 0x07, 0x4b, 0x0a, 0x1a, 0x4c, 0x41, 0x4d, 0x1f, 0x1d, 0x17, 0x1d, 0x00, 0x15, 0x1b, 0x1d, 0x0f, 0x48, 0x0e, 0x49, 0x1e, 0x02, 0x49, 0x01, 0x0c, 0x15, 0x00, 0x50, 0x11, 0x5c, 0x50, 0x58, 0x50, 0x43, 0x42, 0x03, 0x42, 0x13, 0x54, 0x42, 0x4c, 0x11, 0x50, 0x43, 0x0b, 0x5e, 0x09, 0x4d, 0x14, 0x49, 0x57, 0x08, 0x0d, 0x44, 0x44, 0x25, 0x46, 0x43	};	// Perform the encryption here:	bool good=true;	for (unsigned int i=0;i<length;i++)	{		byte out=plaintext[i] ^ key[i%keylength];		if (out!=ciphertext[i])			good=false;	}	// Dare the checker to find a situation where it's all good	assert(!good);	return 0;}`
Immediately, CBMC finds a solution!  But the solution is plaintext = ciphertext, and key = 0.

The problem is we haven't put any constraints on the solution--if plaintext and key can be anything, there are way too many solutions possible.  In CBMC we can add constraints using an assert-like macro __CPROVER_assume(bool), which will force the uninitialized variables referenced in the boolean expression to conform to the constraints you specify.  You want to do this before doing any calculations on the variables, since __CPROVER_assume doesn't work retroactively.
`/** Break crypto for 100: xor with repeating key.*/typedef unsigned char byte;// Return true if this byte is printable ascii:bool is_printable(byte b) {	if (b>=' ' && b<='~') return true;	return false;}// Return true if this byte is a plausible hex digit:bool is_hex_digit(byte b) {	if (b>='0' && b<='9') return true;	if (b>='a' && b<='f') return true;	else return false;}int main() {	const int length=137; // == 274/2, because the "encrypted" file has 274 bytes of hex	const int hashlen=32; // MD5 hex digits	unsigned int keylength; // unknown	__CPROVER_assume(keylength>=5 && keylength<length-hashlen);	const byte key[keylength]; // unknown		const byte plaintext[length]; // unknown	// Plaintext starts with "flag{":	__CPROVER_assume(plaintext[0]=='f');	__CPROVER_assume(plaintext[1]=='l');	__CPROVER_assume(plaintext[2]=='a');	__CPROVER_assume(plaintext[3]=='g');	__CPROVER_assume(plaintext[4]=='{');	// Key and plaintext are both printable ascii	for (unsigned int k=0;k<keylength;k++) 		__CPROVER_assume(is_printable(key[k]));	for (unsigned int i=0;i<length;i++) 		__CPROVER_assume(is_printable(plaintext[i]));		// Key gets added to plaintext near end:		unsigned int keystart=length-hashlen-keylength;	for (unsigned int k=0;k<keylength;k++)	{		unsigned int i=keystart+k;		__CPROVER_assume(key[k]==plaintext[i]);	}	// Last segment of plaintext is MD5 hex digits, in lowercase:	for (unsigned int i=length-hashlen;i<length;i++) 		__CPROVER_assume(is_hex_digit(plaintext[i]));	const byte ciphertext[length]={		0x27, 0x4c, 0x10, 0x12, 0x1a, 0x01, 0x00, 0x49, 0x5b, 0x50, 0x2d, 0x55, 0x1c, 0x55, 0x7f, 0x0b, 0x08, 0x33, 0x58, 0x5d, 0x1b, 0x27, 0x03, 0x0b, 0x52, 0x28, 0x04, 0x0d, 0x37, 0x53, 0x49, 0x0a, 0x1c, 0x02, 0x54, 0x15, 0x05, 0x15, 0x25, 0x45, 0x51, 0x18, 0x00, 0x19, 0x11, 0x53, 0x4a, 0x00, 0x52, 0x56, 0x0a, 0x14, 0x59, 0x4f, 0x0b, 0x1e, 0x49, 0x0a, 0x01, 0x0c, 0x45, 0x14, 0x41, 0x1e, 0x07, 0x00, 0x14, 0x61, 0x5a, 0x18, 0x1b, 0x02, 0x52, 0x1b, 0x58, 0x03, 0x05, 0x17, 0x00, 0x02, 0x07, 0x4b, 0x0a, 0x1a, 0x4c, 0x41, 0x4d, 0x1f, 0x1d, 0x17, 0x1d, 0x00, 0x15, 0x1b, 0x1d, 0x0f, 0x48, 0x0e, 0x49, 0x1e, 0x02, 0x49, 0x01, 0x0c, 0x15, 0x00, 0x50, 0x11, 0x5c, 0x50, 0x58, 0x50, 0x43, 0x42, 0x03, 0x42, 0x13, 0x54, 0x42, 0x4c, 0x11, 0x50, 0x43, 0x0b, 0x5e, 0x09, 0x4d, 0x14, 0x49, 0x57, 0x08, 0x0d, 0x44, 0x44, 0x25, 0x46, 0x43	};	// Perform the encryption here:	bool good=true;	for (unsigned int i=0;i<length;i++)	{		byte out=plaintext[i] ^ key[i%keylength];		if (out!=ciphertext[i])			good=false;	}	// Dare the checker to find a situation where it's all good	assert(!good);	return 0;}`
This is a valid CBMC program, and in theory it will eventually find the answer, but it takes an unreasonably long time, and uses over 30GB of RAM after half an hour.

One of the big problems with SAT is data-dependent indexing.  The solver basically builds a big multiplexor circuit to fake each data-dependent array indexing operation, which takes a lot of time and RAM.  Here, all our data-dependent indexing is happening on the key, because we don't know the key's length.  (This is a situation where a fixed-length block cipher is easier to cryptanalyze.)

We can make CBMC's job much easier if we can figure out the key length.  We've recovered the first 5 chars of the key because we know how the plaintext starts, so checking the decrypted text at all possible key lengths we get a bunch of garbage, and a tiny amount of plausible text at just the right keylength:
```keylength=5	  	  @ 8.1	  lum 	  J(B-<	  Zr~3	  i\$|B2	  *mw5	  T%dP\$	  8qlp	  jq'7	  K4(:j	  _i{tm	  40kf	  A4/y	  Z"#n9	  B%fuc	  Fk{o-	  \00mnhv	  \ dn|	  Nh<	  Cipyt	  Ap`)1	  p27b	  3%7-	  Pp2~?	  Hme<6	  I-51D	  ckeylength=6	  	  Ai*%L	  ]u~i	  }jRb	  uxV	  *mw5	  D5T00	  A9`&+	  v{a8	  J>8`	  40kf	  UA+mz	  ;)vd	  A"v>k
a<j|	  \ dn|	  	.8kc	  @,du1	  p)%"	  Bbb!#	  Pp2~?	  48"i	  dT3"keylength=7	  	  {!X4	  >+yF9	  f#z'I	  vs8}	  T%dP\$	  A9`&+	  *e,.	  *py\$	  _'qa\00	  Z"#n9	  V sr*
a<j|	  A5jhn	  >s<`	  Ap`)1	  br7r
1!6j	  48"i	  76keylength=8	  	  p\ }	  I)(z	  uxV	  ]"%`d	  8qlp	  v{a8	  *py\$	  F e;	  ;)vd	  Fk{o-	  \7lut	  	.8kc	  T !d=	  br7r	  Pp2~?	  wyx%	  keylength=9	  	  
\$i4	  }jRb	  L"<k	  D5T00	  jq'7	  J>8`	  _'qa\00	  ;)vd	  *k9 	  \ dn|	  _"8tm	  p)%"	  b=d1	  48"i	  ckeylength=10	  	  lum 	  Zr~3	  *mw5	  8qlp	  K4(:j	  40kf	  Z"#n9	  Fk{o-	  \ dn|	  Cipyt	  p27b	  Pp2~?	  I-51Dkeylength=11	  	  <\$j	  B+#]e	  Ctdpt	  Ps;u3	  _i{tm	  UA+mz	  V sr*	  \7lut	  _"8tm	  p27b	  cz+h	  dT3"keylength=12	  	  ]u~i	  uxV	  D5T00	  v{a8	  40kf	  ;)vd
a<j|	  	.8kc	  p)%"	  Pp2~?	  dT3"keylength=13	  	  _z}R	  E-F&(	  qiux	  ozk(	  A4/y	  A"v>k	  A5jhn	  T !d=	  b=d1	  I-51Dkeylength=14	  	  >+yF9	  vs8}	  A9`&+	  *py\$	  Z"#n9
a<j|	  >s<`	  br7r	  48"ikeylength=15	  	  J(B-<	  *mw5	  jq'7	  40kf	  B%fuc	  \ dn|	  Ap`)1	  Pp2~?	  ckeylength=16	  	  I)(z	  ]"%`d	  v{a8	  F e;	  Fk{o-	  	.8kc	  br7r	  wyx%keylength=17	  	  rx,nF	  5t`D	  Uy>~	  8jw3	  \00mnhv	  @,du1
1!6j	  keylength=18	  	  }jRb	  D5T00	  J>8`	  ;)vd	  \ dn|	  p)%"	  48"ikeylength=19	  	  ;Vvj	  de ma	  K!}0u	  D7qwf	  Nh<	  Bbb!#	  76keylength=20	  	  Zr~3	  8qlp	  40kf	  Fk{o-	  Cipyt	  Pp2~?keylength=21	  	  f#z'I	  A9`&+	  _'qa\00
a<j|	  Ap`)1	  48"ikeylength=22	  	  B+#]e	  Ps;u3	  UA+mz	  \7lut	  p27b	  dT3"keylength=23	  	  JrYql	   ##k	  Y;s'z	  T;lz)	  3%7-keylength=24	  	  uxV	  v{a8	  ;)vd	  	.8kc	  Pp2~?keylength=25	  	  i\$|B2	  K4(:j	  B%fuc	  Cipyt	  Hme<6keylength=26	  	  E-F&(	  ozk(	  A"v>k	  T !d=	  I-51Dkeylength=27	  	  L"<k	  J>8`	  *k9 	  p)%"	  ckeylength=28	  	  vs8}	  *py\$
a<j|	  br7rkeylength=29	  	  i{ic	  @,4a 	  ^=fha	  Rt39pkeylength=30	  	  *mw5	  40kf	  \ dn|	  Pp2~?keylength=31	  	  K<s!t	  \00>vuu	  Z=~=o	  )<a(keylength=32	  	  ]"%`d	  F e;	  	.8kc	  wyx%keylength=33	  	  Ctdpt	  UA+mz	  _"8tm	  dT3"keylength=34	  	  5t`D	  8jw3	  @,du1	  keylength=35	  	  T%dP\$	  Z"#n9	  Ap`)1keylength=36	  	  D5T00	  ;)vd	  p)%"keylength=37	  	  T4\$y	  #tba	  c3v#keylength=38	  	  de ma	  D7qwf	  Bbb!#keylength=39	  	  qiux	  A"v>k	  b=d1keylength=40	  	  8qlp	  Fk{o-	  Pp2~?keylength=41	  	  Y hd2	  K:=4,	  J~x8ukeylength=42	  	  A9`&+
a<j|	  48"ikeylength=43	  	  X1"?a	  ?lb|	  (|1%keylength=44	  	  Ps;u3	  \7lut	  dT3"keylength=45	  	  jq'7	  \ dn|	  ckeylength=46	  	   ##k	  T;lz)keylength=47	  	  Ar'u	  \/9{(keylength=48	  	  v{a8	  	.8kckeylength=49	  	  *e,.	  >s<`keylength=50	  	  K4(:j	  Cipytkeylength=51	  	  Uy>~	  @,du1keylength=52	  	  ozk(	  T !d=keylength=53	  	  +o<k	  1-%9keylength=54	  	  J>8`	  p)%"keylength=55	  	  _i{tm	  p27bkeylength=56	  	  *py\$	  br7rkeylength=57	  	  K!}0u	  Bbb!#keylength=58	  	  @,4a 	  Rt39pkeylength=59	  	  Mee4	  l`%"keylength=60	  	  40kf	  Pp2~?keylength=61	  	  Uaora	  +/|,keylength=62	  	  \00>vuu	  )<a(keylength=63	  	  _'qa\00	  48"ikeylength=64	  	  F e;	  wyx%keylength=65	  	  A4/y	  I-51Dkeylength=66	  	  UA+mz	  dT3"keylength=67	  	   zinc	  df2keylength=68	  	  8jw3	  keylength=69	  	  Y;s'zkeylength=70	  	  Z"#n9keylength=71	  	  Crj-bkeylength=72	  	  ;)vdkeylength=73	  	  Zxrpvkeylength=74	  	  #tbakeylength=75	  	  B%fuckeylength=76	  	  D7qwfkeylength=77	  	  V sr*keylength=78	  	  A"v>kkeylength=79	  	  C':{keylength=80	  	  Fk{o-keylength=81	  	  *k9 keylength=82	  	  K:=4,keylength=83	  	  [l08~keylength=84
a<j|keylength=85	  	  \00mnhvkeylength=86	  	  ?lb|keylength=87	  	  ^=fhakeylength=88	  	  \7lutkeylength=89	  	  V=q`zkeylength=90	  	  \ dn|keylength=91	  	  A5jhnkeylength=92	  	  T;lz)keylength=93	  	  Z=~=okeylength=94	  	  \/9{(keylength=95	  	  Nh<keylength=96	  	  	.8kckeylength=97	  	  Oiow(keylength=98	  	  >s<`keylength=99	  	  _"8tmkeylength=100	  	  Cipytkeylength=101	  	  !}`akeylength=102	  	  @,du1keylength=103	  	  M5q%pkeylength=104	  	  T !d=keylength=105	  	  Ap`)1keylength=106	  	  1-%9keylength=107	  	  P|!-1keylength=108	  	  p)%"keylength=109	  	  x!6#keylength=110	  	  p27bkeylength=111	  	  c3v#keylength=112	  	  br7rkeylength=113	  	  #3f5keylength=114	  	  Bbb!#keylength=115	  	  3%7-keylength=116	  	  Rt39pkeylength=117	  	  b=d1keylength=118	  	  l`%"keylength=119
1!6jkeylength=120	  	  Pp2~?keylength=121	  	  cz+hkeylength=122	  	  +/|,keylength=123	  	  J~x8ukeylength=124	  	  )<a(keylength=125	  	  Hme<6keylength=126	  	  48"ikeylength=127	  	  Ui&}lkeylength=128	  	  wyx%keylength=129	  	  (|1%keylength=130	  	  I-51Dkeylength=131	  	  Ld5P'keylength=132	  	  dT3"keylength=133	  	  76keylength=134	  	  df2keylength=135	  	  ckeylength=136	  	  ```
The only all-printable keylength is 67, so inserting keylength=67 into our CBMC program above, it only takes 2.3 seconds to find the plaintext and key:

`State 21 file decrypt.cpp line 24 function main thread 0----------------------------------------------------  key={ 65, 32, 113, 117, 97, 114, 116, 32, 106, 97, 114, 32, 111, 102, 32, 111, 105, 108, 32, 109, 105, 120, 101, 100, 32, 119, 105, 116, 104, 32, 122, 105, 110, 99, 32, 111, 120, 105, 100, 101, 32, 109, 97, 107, 101, 115, 32, 97, 32, 118, 101, 114, 121, 32, 98, 114, 105, 103, 104, 116, 32, 112, 97, 105, 110, 116, 124 } State 22 file decrypt.cpp line 26 function main thread 0----------------------------------------------------  plaintext={ 102, 108, 97, 103, 123, 115, 116, 105, 49, 49, 95, 117, 115, 51, 95, 100, 97, 95, 120, 48, 114, 95, 102, 111, 114, 95, 109, 121, 95, 115, 51, 99, 114, 97, 116, 122, 125, 124, 65, 32, 113, 117, 97, 114, 116, 32, 106, 97, 114, 32, 111, 102, 32, 111, 105, 108, 32, 109, 105, 120, 101, 100, 32, 119, 105, 116, 104, 32, 122, 105, 110, 99, 32, 111, 120, 105, 100, 101, 32, 109, 97, 107, 101, 115, 32, 97, 32, 118, 101, 114, 121, 32, 98, 114, 105, 103, 104, 116, 32, 112, 97, 105, 110, 116, 124, 100, 53, 49, 49, 49, 51, 53, 48, 98, 98, 98, 101, 49, 48, 53, 49, 50, 49, 98, 57, 97, 57, 52, 57, 54, 97, 99, 48, 56, 100, 102, 50 } ...Violated property:  file decrypt.cpp line 67 function main  assertion  !goodVERIFICATION FAILED`
We can then dump the recovered plaintext as ASCII with a simple C++ program:
```char buf[]={
102, 108, 97, 103, 123, 115, 116, 105, 49, 49, 95, 117, 115, 51, 95, 100, 97, 95, 120, 48, 114, 95, 102, 111, 114, 95, 109, 121, 95, 115, 51, 99, 114, 97, 116, 122, 125, 124, 65, 32, 113, 117, 97, 114, 116, 32, 106, 97, 114, 32, 111, 102, 32, 111, 105, 108, 32, 109, 105, 120, 101, 100, 32, 119, 105, 116, 104, 32, 122, 105, 110, 99, 32, 111, 120, 105, 100, 101, 32, 109, 97, 107, 101, 115, 32, 97, 32, 118, 101, 114, 121, 32, 98, 114, 105, 103, 104, 116, 32, 112, 97, 105, 110, 116, 124, 100, 53, 49, 49, 49, 51, 53, 48, 98, 98, 98, 101, 49, 48, 53, 49, 50, 49, 98, 57, 97, 57, 52, 57, 54, 97, 99, 48, 56, 100, 102, 50
,0 };
puts(buf);
return 0;```

(Try this in NetRun now!)

This prints:
`flag{sti11_us3_da_x0r_for_my_s3cratz}|A quart jar of oil mixed with zinc oxide makes a very bright paint|d5111350bbbe105121b9a9496ac08df2`
It only takes about 2 seconds for CBMC to check a given keylength, and invalid key lengths won't decrypt properly (assert(!good) always passes), so you can exhaustively check all the lengths in a few minutes even if you couldn't figure them out by inspection.  This shell script substitutes "keylength=META;" in the source code with each different number, runs CBMC, and checks if it worked:
`#!/bin/sh# Bruteforce the variable META by substituting in different values.len=5while [ "\$len" -lt 130 ]do	sed -e "s/META/\$len/g" meta_decrypt.cpp > a.cpp	cbmc a.cpp > meta_log	if [ \$? -eq 0 ]	then		echo "No solutions for length \$len"	else		echo "SOLUTION FOUND for length \$len"		cp meta_log meta_solution_\$len	fi	len=`expr \$len + 1`done`
CBMC should really be smart enough to bruteforce the key length this way itself, since internally it unwinds loops using a similar guess-and-check approach.

## CBMC for Reversing

Example challenge: realism, Reversing for 400 in CSAW 2017 CTF

A typical reversing challenge has this structure:
`	read user input	if (crazy_processing(input))		print "That's the flag!"	else		print "Nope"`
Normally the input space is too huge to brute force search.

Bounded model checkers are useful for automating the search for an input that satisfies the crazy processing.  A general algorithm for solving reversing problems is to encode the processing as a SAT instance.

For example, the realism boot block boils down to some fairly simple SSE operations, like shuffles and bitwise AND, whose output is then compared byte-for-byte with a fixed mask.  A few hours of staring at the disassembly and doublechecking assumptions using a combination of a debugger and NetRun assembly, and we had the program's processing captured in C++:
`/** Bounded model checker program to satisfy  the CSAW CTF reversing problem "realism", by using a SAT solver. Designed for CBMC 4.5. To find the flags, run    cbmc cbmc_flag.cpp and search for the "flags" array in the output. CBMC prints the located values in decimal and binary,  see "flag_checker.cpp" to print it in ASCII.*/const static unsigned int bootblock[4]={	0xcd0013b8, 0xc0200f10, 0x83fbe083, 0x220f02c8};// ; masks: pulled by 00007C91:  andps xmm2,oword [si+0x7d90]const static unsigned int mask[9][4]={	{0xffffff00, 0xffffffff, 0xffffff00, 0xffffffff},	{0xffffffff, 0x00ffffff, 0xffffffff, 0x00ffffff},	{0xffffffff, 0xff00ffff, 0xffffffff, 0xff00ffff},	{0xffffffff, 0xffff00ff, 0xffffffff, 0xffff00ff},	{0xffffffff, 0xffffff00, 0xffffffff, 0xffffff00},	{0x00ffffff, 0xffffffff, 0x00ffffff, 0xffffffff},	{0xff00ffff, 0xffffffff, 0xff00ffff, 0xffffffff},	{0xffff00ff, 0xffffffff, 0xffff00ff, 0xffffffff},	{0xffffff00, 0xffffffff, 0xffffff00, 0xffffffff}};//byte distance sum targets: ; pulled by 00007CB2:  cmp edi,[edx+0x7da8]const static unsigned int targets[8]={	0x02110270, 0x02290255, 0x025e0291, 0x01f90233,	0x027b0278, 0x02090221, 0x0290025d, 0x02df028f};int main() {	unsigned int flag[4]; // <- uninitialized (essentially tries all flags)/*00007C86  660F70C01E        pshufd xmm0,xmm0,0x1e ; shuffle flag as DWORDS:0x1e:  00 01 11 10*/	unsigned int xmm0[4]; // shuffled flag bytes	xmm0[0]=flag[2];	xmm0[1]=flag[3];	xmm0[2]=flag[1];	xmm0[3]=flag[0];		unsigned int xmm5[4];	for (int i=0;i<4;i++) xmm5[i]=bootblock[i];		bool OK=true;	int si=8;	do{		// 00007C91  0F5494907D        andps xmm2,oword [si+0x7d90]		unsigned int xmm2[4];		for (int i=0;i<4;i++) xmm2[i]=xmm0[i]&mask[si][i];			// 00007C96  660FF6EA          psadbw xmm5,xmm2		unsigned short diffL=0, diffH=0; // sum of absolute differences		for (int word=0;word<4;word++) 		for (int b=0;b<4;b++) {			unsigned short A=0xFF&((xmm2[word])>>(8*b));			// Force printable ASCII:			// __CPROVER_assume(A==0 || (A>=0x20 && A<0x7F));			unsigned short B=0xFF&((xmm5[word])>>(8*b));			short diff=A-B;			if (diff<0) diff=-diff; // absolute value			if (word<2) diffL+=diff;			else        diffH+=diff;		}				// psadbw overwrites xmm5 with the differences:		xmm5[0]=diffL;		xmm5[1]=0;		xmm5[2]=diffH;		xmm5[3]=0;		// Crazy code at 0x7C9A-7CA7 to loads up diffs as integer register:			unsigned int sumdiff2=(diffL<<16) + diffH;			// Compare at 0x7CB2:		int dx=si;		dx--;		unsigned int target_val=targets[dx];		if (sumdiff2!=target_val) OK=false;		//printf("target %08x, actual %08x\n",target_val,sumdiff2);			si--;	} while (OK && si>0);	assert(!OK);}`
CBMC takes under one second to find:
`State 18 file cbmc_flag_finder.cpp line 40 function main thread 0----------------------------------------------------  flag={ 863122555u, 1601858657u, 862204013u, 2100328799u } `
Again, we can print as ASCII with:
```unsigned int flag[]={ 863122555u, 1601858657u, 862204013u, 2100328799u,0 };
puts((char *)flag);
```

(Try this in NetRun now!)

This prints:
`{4r3alz_m0d3_y0}`
("for realz mode, yo")

The first four bytes are always 'flag', and weren't touched in downstream procesing, so we didn't bother including them in CBMC.

One drawback of CBMC at the moment is its very limited understanding of pointer type conversion; above we extract bytes using bit shifts rather than just typecasting a pointer to (char *), because CBMC has no idea what the (char *) typecast is doing to the underlying integers.  This means you should stick to a single type, here integers, rather than switching back and forth between types using pointers (as seems natural to a programmer sufficiently poisoned by working in assembly language).