Remote Attestation is emerging as a promising technique to ensure that some remote device is in a trustworthy state. This can for example be an IoT device that is attested by a cloud service before allowing the device to connect. However, flaws in the communication protocols associated with the remote attestation mechanism can introduce vulnerabilities into the system design and potentially nullify the added security. Formal verification of protocol security can help to prevent such flaws. In this work we provide a detailed analysis of the necessary security properties for remote attestation focusing on the authenticity of the involved agents. We extend beyond existing work by considering the possibility of an attestation server (making the attestation process involve three parties) as well as requiring verifier authentication. We demonstrate that some security properties are not met by a state-of-the-art commercial protocol for remote attestation for our strong adversary model. Moreover, we design two new communication protocols for remote attestation that we formally prove fulfil all of the considered authentication properties.

Providing authenticated interactions is a key responsibility of most cryptographic protocols. When designing new protocols with strict security requirements it is therefore essential to formally verify that they fulfil appropriate authentication properties. We identify a gap in the case of protocols with unilateral (one-way) authentication, where existing properties are poorly adapted. In existing work, there is a preference for defining strong authentication properties, which is good in many cases but not universally applicable. In this work we make the case for weaker authentication properties. In particular, we investigate one-way authentication and extend Lowe's authentication hierarchy with two such properties. We formally prove the relationship between the added and existing properties. Moreover, we demonstrate the usefulness of the added properties in a case study on remote attestation protocols. This work complements earlier work with additional generic properties that support formal verification of a wider set of protocol types.

Code obfuscation is an important topic, both in terms of defense, when trying to prevent intellectual property theft, and from the offensive point of view, when trying to break obfuscation used in malware. Several recent works have discussed techniques for preventing or delaying reverse engineering of binaries. While most works focus on methods that obscure program logic, the complimentary approach of disassembly desynchronization has received relatively little attention, despite being often used by, for example, malware authors. The technique puts another hurdle in the way of attackers by targeting the most fundamental step of the reverse-engineering process: recovering assembly code from a program binary. In the interest of furthering research into this kind of obfuscation, we present desync-cc, a tool for automatic application of disassembly desynchronization. To facilitate maximal ease-of-use, the tool is designed as a drop-in replacement for gcc, and works by intercepting and modifying intermediate assembly-code during compilation.

Code obfuscation is an important topic, both in terms of defense, when trying to prevent intellectual property theft, and from the offensive point of view, when trying to break obfuscation used by malware authors to hide their malicious intents. Consequently, several works in recent years have discussed techniques that aim to prevent or delay reverse-engineering of binaries. While most works focus on methods that obscure the program logic from potential attackers, the complimentary approach of disassembly desynchronization has received relatively little attention. This technique puts another hurdle in the way of attackers by targeting the most fundamental step of the reverse-engineering process: recovering assembly code from a program binary. The technique works by tricking a disassembler into decoding the instruction stream at an invalid offset. On CPU architectures with variable-length instructions, this often yields valid albeit meaningless assembly code, while hiding a part of the original code. In the interest of furthering research into disassembly desynchronization, both from a defensive and offensive point of view, we have created desync-cc, a tool for automatic application of disassembly-desynchronization obfuscation. The tool is designed as a drop-in replacement for gcc, and works by intercepting and modifying intermediate assembly code during compilation. By applying obfuscation after the code generation phase, our tool allows a much more granular control over where obfuscation is applied, compared to a source-code level obfuscator. In this paper, we describe the design and implementation of desync-cc, and present a preliminary evaluation of its effectiveness and efficiency on a number of real-world Linux programs.