Using SAT solvers and brute force approach to recover AES key from partial key schedule images

Recovering an AES key exploiting the redundancy of key material inherent in the AES key schedule is a topic widely discussed in the scientific literature. Specifically, there are many papers that analyze the aforementioned problem starting from a corrupt key schedule, this scenario is very frequent if a cold boot attack is carried out in which a corrupt dump of the ram memory is performed. In these articles, different techniques are used to derive the AES key including the use of SAT solver and MAX SAT solver, tools that aim to solve the problem of Boolean satisfiability. In this thesis, on the other hand, we want to analyze a more general case, i.e., starting from a partial key schedule and obtaining its AES key. Different techniques will be analyzed and combined including the use of SAT solver tools, and brute force algorithm, with the aim of minimizing the time for key recovery.