Automated Detection of Cryptographic Inconsistencies in Android’s Keymaster Implementations

Android smartphones use a dedicated component, Keymaster, to perform all their cryptographic, security-sensitive operations (e.g., storing cryptographic material and performing signing operations). While all Android Keymaster implementations need to expose a specific interface, their internals are hard to analyze, since their source code is generally not available. Moreover, Android Keymasters' code normally runs in a Trusted Execution Environment (TEE), where typical debugging functionality is not available. For these reasons, Keymaster implementations cannot be analyzed using white-box or gray-box automated approaches.