Using MaxSAT to Correct Errors in AES Key Schedule Images

Cold boot attack is a side channel attack that recovers data from memory, which persists for a short period after power is lost. In the course of this attack, the memory gradually degrades over time and only a corrupted version of the data may be available to the attacker. Recently, great efforts have been devoted to reconstructing the original data from a corrupted version of AES key schedules, based on the assumption that all bits in the charged states tend to decay to the ground states while no bit in the ground state ever inverts. However, in practice, there is a small number of bits flipping in the opposite direction, called reverse flipping errors. In this paper, motivated by the latest work that formulates the relations of AES key bits as a Boolean Satisfiability problem, we move one step further by taking the reverse flipping errors into consideration and employing an off-the-shelf MaxSAT solver to accomplish the key recovery of AES-128 key schedules from decayed memory images. Specifically, a MaxSAT solver takes the relations of key bits as hard constraints and the bits in the charged states as soft constraints, then it tries to satisfy all the hard constraints and as many soft constraints as possible by eliminating the unsatisfied minority. Experimental results show that, in the presence of reverse flipping errors, the MaxSAT approach enables reliable recovery of key schedules with significantly less time, compared with the SAT approach that relies on brute force search to find out the target errors.