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-<	  Zr~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	  c
keylength=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	  76
keylength=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	  c
keylength=10	  	  lum 	  Zr~3	  *mw5	  8qlp	  K4(:j	  40kf	  Z"#n9	  Fk{o-	  \ dn|	  Cipyt	  p27b	  Pp2~?	  I-51D
keylength=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-51D
keylength=14	  	  >+yF9	  vs8}	  A9`&+	  *py$	  Z"#n9	  
a<j|	  >s<`	  br7r	  48"i
keylength=15	  	  J(B-<	  *mw5	  jq'7	  40kf	  B%fuc	  \ dn|	  Ap`)1	  Pp2~?	  c
keylength=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"i
keylength=19	  	  ;Vvj	  de ma	  K!}0u	  D7qwf	  Nh<	  Bbb!#	  76
keylength=20	  	  Zr~3	  8qlp	  40kf	  Fk{o-	  Cipyt	  Pp2~?
keylength=21	  	  f#z'I	  A9`&+	  _'qa\00	  
a<j|	  Ap`)1	  48"i
keylength=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<6
keylength=26	  	  E-F&(	  ozk(	  A"v>k	  T !d=	  I-51D
keylength=27	  	  L"<k	  J>8`	  
*k9 	  p)%"	  c
keylength=28	  	  vs8}	  *py$	  
a<j|	  br7r
keylength=29	  	  i{ic	  @,4a 	  ^=fha	  Rt39p
keylength=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`)1
keylength=36	  	  D5T00	  ;)vd	  p)%"
keylength=37	  	  T4$y	  #tba	  c3v#
keylength=38	  	  de ma	  D7qwf	  Bbb!#
keylength=39	  	  qiux	  A"v>k	  b=d1
keylength=40	  	  8qlp	  Fk{o-	  Pp2~?
keylength=41	  	  Y hd2	  K:=4,	  J~x8u
keylength=42	  	  A9`&+	  
a<j|	  48"i
keylength=43	  	  X1"?a	  ?lb|	  (|1%
keylength=44	  	  Ps;u3	  \7lut	  dT3"
keylength=45	  	  jq'7	  \ dn|	  c
keylength=46	  	   ##k	  T;lz)
keylength=47	  	  Ar'u	  \/9{(
keylength=48	  	  v{a8	  	.8kc
keylength=49	  	  *e,.	  >s<`
keylength=50	  	  K4(:j	  Cipyt
keylength=51	  	  Uy>~	  @,du1
keylength=52	  	  ozk(	  T !d=
keylength=53	  	  +o<k	  1-%9
keylength=54	  	  J>8`	  p)%"
keylength=55	  	  _i{tm	  p27b
keylength=56	  	  *py$	  br7r
keylength=57	  	  K!}0u	  Bbb!#
keylength=58	  	  @,4a 	  Rt39p
keylength=59	  	  Mee4	  l`%"
keylength=60	  	  40kf	  Pp2~?
keylength=61	  	  Uaora	  +/|,
keylength=62	  	  \00>vuu	  )<a(
keylength=63	  	  _'qa\00	  48"i
keylength=64	  	  F e;	  wyx%
keylength=65	  	  A4/y	  I-51D
keylength=66	  	  UA+mz	  dT3"
keylength=67	  	   zinc	  df2
keylength=68	  	  8jw3	  
keylength=69	  	  Y;s'z
keylength=70	  	  Z"#n9
keylength=71	  	  Crj-b
keylength=72	  	  ;)vd
keylength=73	  	  Zxrpv
keylength=74	  	  #tba
keylength=75	  	  B%fuc
keylength=76	  	  D7qwf
keylength=77	  	  V sr*
keylength=78	  	  A"v>k
keylength=79	  	  C':{
keylength=80	  	  Fk{o-
keylength=81	  	  
*k9 
keylength=82	  	  K:=4,
keylength=83	  	  [l08~
keylength=84	  	  
a<j|
keylength=85	  	  \00mnhv
keylength=86	  	  ?lb|
keylength=87	  	  ^=fha
keylength=88	  	  \7lut
keylength=89	  	  V=q`z
keylength=90	  	  \ dn|
keylength=91	  	  A5jhn
keylength=92	  	  T;lz)
keylength=93	  	  Z=~=o
keylength=94	  	  \/9{(
keylength=95	  	  Nh<
keylength=96	  	  	.8kc
keylength=97	  	  Oiow(
keylength=98	  	  >s<`
keylength=99	  	  _"8tm
keylength=100	  	  Cipyt
keylength=101	  	  !}`a
keylength=102	  	  @,du1
keylength=103	  	  M5q%p
keylength=104	  	  T !d=
keylength=105	  	  Ap`)1
keylength=106	  	  1-%9
keylength=107	  	  P|!-1
keylength=108	  	  p)%"
keylength=109	  	  x!6#
keylength=110	  	  p27b
keylength=111	  	  c3v#
keylength=112	  	  br7r
keylength=113	  	  #3f5
keylength=114	  	  Bbb!#
keylength=115	  	  3%7-
keylength=116	  	  Rt39p
keylength=117	  	  b=d1
keylength=118	  	  l`%"
keylength=119	  	  
1!6j
keylength=120	  	  Pp2~?
keylength=121	  	  cz+h
keylength=122	  	  +/|,
keylength=123	  	  J~x8u
keylength=124	  	  )<a(
keylength=125	  	  Hme<6
keylength=126	  	  48"i
keylength=127	  	  Ui&}l
keylength=128	  	  wyx%
keylength=129	  	  (|1%
keylength=130	  	  I-51D
keylength=131	  	  Ld5P'
keylength=132	  	  dT3"
keylength=133	  	  76
keylength=134	  	  df2
keylength=135	  	  c
keylength=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
  !good

VERIFICATION 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=5
while [ "$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).