イベント情報

ハイブリッド開催（会場およびオンライン）
　【会場】学術情報メディアセンター南館　2階　202マルチメディア講義室
（授乳室を設置しています。ご利用の場合は事務室（電話番号075-753-7400）に
お申し付けください。）
　　　　　本部構内マップ［93番］
　【オンライン】 Zoom を使用します。

主催：京都大学 学術情報メディアセンター

京都大学 学術情報メディアセンター　小谷 　大祐
kotani * media.kyoto-u.ac.jp　（*を＠に変えてください）

◆15時00分～16時00分　【会場にて講演】【使用言語：英語、同時通訳：なし】
講演者： Binoy Ravindran (Virginia Tech)　
講演題目： A Step Toward Trustworthy Binary Verification at Scale.
講演概要： Many production legacy software systems are available only in binary form.
This is due to several reasons including intellectual property and proprietary issues,
outdated build processes and environments, and third-party libraries and tools
that are no longer available or backwards compatible. Security vulnerability analysis of such software is still a necessary task due to the need to rapidly patch program errors, especially those that can be used to create security exploits, i.e., unintended, or malicious behaviors or leak sensitive data. A large body of work has focused on this problem space including disassembly, decompilation, and binary verification, among others. A common denominator of these approaches is binary lifting: raw unstructured data is lifted to a form for reasoning over behavior and semantics. Majority of existing binary lifting approaches are untrustworthy (e.g., misses jump targets, misidentifies code as data), which negatively affects the trust base of techniques that rely on them.
In this talk, I will present an approach for trustworthy binary lifting. The technique simultaneously disassembles, recovers control flow, and verifies a class of security properties including return address integrity, bounded control flow, and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains
an over-approximation of all possible execution paths of the binary. The lifted representation contains proof obligations that are sufficient to formally prove (e.g., using a theorem-prover)
the security properties and correctness of the lifted representation, which removes the lifting algorithm and its implementation from the trust base. We apply this approach to Linux Foundation’s Xen Hypervisor covering about 400K instructions, providing evidence of its effectiveness and scalability for trustworthy binary lifting of off-the-shelf production software.
I will argue that such a binary lifting technique not only improves the trust base of downstream techniques (e.g., binary verification) but also exposes novel ways for reasoning about related problems (e.g., binary patching).