A Formally Verified Digital Signature Device for Smartphones

Attacks on Internet banking using a malware called “High Roller” triggered the EU cyber security agency to issue a warning and call for action. With the proliferation of smartphones, customers want to do online banking on their phone, too. But a smartphone could also be compromised and so the customer cannot trust what is shown in the display and PINs could be sent to the attacker. We assume an attacker motivated by financial gain through diverting manipulated bank transactions to an account under his control. Based on that assumption, we propose signed transaction summaries where the signature is created in a separate security device after the summary has been shown to the user and the user has approved it. Keeping the requirements to the absolute minimum, we derive a hardware implementation for the Jolla smartphone and, based on that hardware, a secure software implementation. We use commercial off-the-shelf components and, by keeping the protocols simple, reduce the trusted computing base as much as possible. We then demonstrate how the program in the micro controller avoids common software flaws and show fragments of a formal verification of the correctness of the microcontroller program.