Problem description:
Advanced Encryption Standard (AES) is a specification for the
encryption of electronic data established by NIST, and is currently
used as a worldwide prevalent symmetric cryptographic algorithm. Since
2008, with the advent of cold boot attack [1], a new threat has been
posed to systems that store sensitive data in memory, including AES.
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. The AES key
recovery problem is to reconstruct the original key bits from a
corrupted version of AES key schedules, based on the observation that
most memory bits in the charged states (encoded as 1) tend to decay to
the ground states (encoded as 1) as time goes on, with a constant and
small fraction of bits flipping to the charged states. Such small
number of reversely flipping bit is called reverse flipping error. In
this scenario, the majority of 1s are correct, with only a small
fraction of 1s flipping from 0, and the goal is to find out such
reverse flipping errors and recover the true bits.

MaxSAT encoding:
Following earlier approaches in literature [2], we use a
straightforward strategy for encoding AES key recovery problem into
partial MaxSAT: relations of key bits are represented by a set of hard
clauses and key bits equal to 1 in the decayed AES key schedule are
represented by a set of soft clauses. Thus, the possibility that the
present 1s may be incorrent is taken into consideration.  Solving the
partial MaxSAT problem amounts to finding an assignment of variables
that satisfy all hard clauses and the maximum number of soft
clauses. As long as the reverse flipping errors account for a small
percentage among all 1s, they can be surely cleared by a partial
MaxSAT solver, which always satisfies the majority of soft clauses by
excluding the unsatisfied minority.

Reference:
[1] J. A. Halderman, S. D. Schoen, N. A. Heninger, W. Clarkson,
W. Paul, J. A. Calandrino, A. J. Feldman, J. Appelbaum, and
E. W. Felten, “Lest we remember: Cold-boot attacks on encryption
keys,” Proc. of USENIX USENIX Security Symposium (SEC’08),
California, USA.
[2] X. Liao, H. Zhang, M. Koshimura, H. Fujita, and R. Hasegawa,
“Using maxsat to correct errors in aes key schedule images,”
Proc. of International Conference on Tools with Artificial
Intelligence (ICTAI’13), pp.284–291, Nov 2013.