Georgios Portokalidis

Chengbin Pang, Ruotong Yu, Yaohui Chen et al.

Disassembly of binary code is hard, but necessary for improving the security of binary software. Over the past few decades, research in binary disassembly has produced many tools and frameworks, which have been made available to researchers and security professionals. These tools employ a variety of strategies that grant them different characteristics. The lack of systematization, however, impedes new research in the area and makes selecting the right tool hard, as we do not understand the strengths and weaknesses of existing tools. In this paper, we systematize binary disassembly through the study of nine popular, open-source tools. We couple the manual examination of their code bases with the most comprehensive experimental evaluation (thus far) using 3,788 binaries. Our study yields a comprehensive description and organization of strategies for disassembly, classifying them as either algorithm or else heuristic. Meanwhile, we measure and report the impact of individual algorithms on the results of each tool. We find that while principled algorithms are used by all tools, they still heavily rely on heuristics to increase code coverage. Depending on the heuristics used, different coverage-vs-correctness trade-offs come in play, leading to tools with different strengths and weaknesses. We envision that these findings will help users pick the right tool and assist researchers in improving binary disassembly.

Georgios Kontaxis, Angelos D. Keromytis, Georgios Portokalidis

Social networking services have attracted millions of users, including individuals, professionals, and companies, that upload massive amounts of content, such as text, pictures, and video, every day. Content creators retain the intellectual property (IP) rights on the content they share with these networks, however, very frequently they implicitly grant them, a sometimes, overly broad license to use that content, which enables the services to use it in possibly undesirable ways. For instance, Facebook claims a transferable, sub-licensable, royalty-free, worldwide license on all user-provided content. Professional content creators, like photographers, are particularly affected. In this paper we propose a design for decoupling user data from social networking services without any loss of functionality for the users. Our design suggests that user data are kept off the social networking service, in third parties that enable the hosting of user-generated content under terms of service and overall environment (e.g., a different location) that better suit the user's needs and wishes. At the same time, indirection schemata are seamlessly integrated in the social networking service, without any cooperation from the server side necessary, so that users can transparently access the off-site data just as they would if hosted in-site. We have implemented our design as an extension for the Chrome Web browser, called Redirect2Own, and show that it incurs negligible overhead on accessing 'redirected' content. We offer the extension as free software and its code as an open-source project.

Yuandong Cyrus Liu, Chengbin Pang, Daniel Dietsch et al.

There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. In this paper we show that similar linear arithmetic approximation of bitvector operations can be done at the source level through transformations. Specifically, we introduce new paths that over-approximate bitvector operations with linear conditions/constraints, increasing branching but allowing us to better exploit the well-developed integer reasoning and interpolation of verification tools. We show that, for reachability of bitvector programs, increased branching incurs negligible overhead yet, when combined with integer interpolation optimizations, enables more programs to be verified. We further show this exploitation of integer interpolation in the common case also enables competitive termination verification of bitvector programs and leads to the first effective technique for LTL verification of bitvector programs. Finally, we provide an in-depth case study of decompiled ("lifted") binary programs, which emulate X86 execution through frequent use of bitvector operations. We present a new tool DarkSea, the first tool capable of verifying reachability, termination, and LTL of lifted binaries.

Chengbin Pang, Ruotong Yu, Dongpeng Xu et al.

Function entry detection is critical for security of binary code. Conventional methods heavily rely on patterns, inevitably missing true functions and introducing errors. Recently, call frames have been used in exception-handling for function start detection. However, existing methods have two problems. First, they combine call frames with heuristic-based approaches, which often brings error and uncertain benefits. Second, they trust the fidelity of call frames, without handling the errors that are introduced by call frames. In this paper, we first study the coverage and accuracy of existing approaches in detecting function starts using call frames. We found that recursive disassembly with call frames can maximize coverage, and using extra heuristic-based approaches does not improve coverage and actually hurts accuracy. Second, we unveil call-frame errors and develop the first approach to fix them, making their use more reliable.

Dimitrios Damopoulos, Georgios Portokalidis

Users with limited use of their hands, such as people suffering from disabilities of the arm, shoulder, and hand (DASH), face challenges when authenticating with computer terminals, specially with publicly accessible terminals such as ATMs. A new glass wearable device was recently introduced by Google and it was immediately welcomed by groups of users, such as the ones described above, as Google Glass allows them to perform actions, like taking a photo, using only verbal commands. This paper investigates whether glass wearable devices can be used to authenticate users, both to grant access (one-time) and to maintain access (continuous), in similar hands-free fashion. We do so by designing and implementing Gauth, a system that enables users to authenticate with a service simply by issuing a voice command, while facing the computer terminal they are going to use to access the service. To achieve this goal, we create a physical communication channel from the terminal to the device using machine readable visual codes, like QR codes, and utilize the device's network adapter to communicate directly with a service. More importantly, we continuously authenticate the user accessing the terminal, exploiting the fact that a user operating a terminal is most likely facing it most of the time. We periodically issue authentication challenges, which are displayed as a QR code on the terminal, that cause the glass device to re-authenticate the user with an appropriate response. We evaluate our system to determine the technical limits of our approach.