Directed Compositional Symbolic Execution for MSP430

Thursday August 31th, 12-1PM @ BA5205

Speaker: Ivan Pustogarov

Title:
Directed Compositional Symbolic Execution for MSP430

Abstract:
As embedded systems become ubiquitous and gradually shift from isolated offline to interconnected online systems, their security becomes a major concern. Embedded systems software is usually written in low-level memory-unsafe programming languages such as C which makes them particularly susceptible to memory corruption vulnerabilities.  In addition, such systems are often equipped with sensors and the firmware controlling them is commonly designed assuming a benign environment which makes them susceptible for signal spoofing attacks.
Symbolic execution is an efficient approach that can help in identifying and understanding these threats: combination of symbolic execution and black-box fuzzing can achieve high code coverage; its ability to automatically generate inputs that drive the program into particular states can be used to better understand possible signal spoofing attacks. Existing symbolic execution tools, however, do not work for firmware code and in contrast to the large body of research for traditional architectures such as x86, there are few tools for lower-end embedded architectures. 
 
In the first part of this talk, I will discuss our experience in building a directed, compositional  symbolic execution framework that targets software for the popular MSP430 family of microcontrollers.  I will give a few more details about our modular approach and  how we tackled interrupt-driven control flow, extensive use of peripheral devices, and hardware-related memory areas that are common for embedded programming and which frustrate traditional symbolic execution tools. I will then describe how we used our tool to partially automate a signal spoofing attack against a recently proposed gesture recognition system to trick the firmware into “recognizing” a gesture of the adversary’s choosing.  In the second part of the talk, I will briefly describe our preliminary work on handling dynamic memory allocation routines
(c/re/malloc) with symbolic sizes that are known to significantly increase the number of execution states if symbolically executed “as-is”.

Bio:
Ivan Pustogarov is a Postdoctoral Researcher at Cornell University where he works on program analysis for security of embedded systems. He received his PhD from the University of Luxembourg with the focus on network security in 2015.
 
His research interests lie in the area of system security and center on program/binary analysis for embedded systems. His recent project focused on developing program analysis tools and techniques for the popular MSP430 family of microcontrollers. His research on network security includes practical low-resource off-path attacks on the Tor and Bitcoin P2P networks. The flaws described in his publications had a direct impact on users’ security and caused redesign of parts of the Tor protocol and its core code. His research has been published in S&P, CCS, AsiaCCS, ESORICS etc., and received attention from the media including BBC, The Register, Dailydot, and others.

How to Learn Klingon Without a Dictionary: Detection and Measurement of Black Keywords Used by the Underground Economy

Thursday Aug 3rd, 12-1PM @ BA5205

Speaker: Prof Haixin Duan from Tsinghua

Title:
How to Learn Klingon Without a Dictionary: Detection and Measurement of Black Keywords Used by the Underground Economy

Abstract:
Online underground economy is an important channel that connects the merchants of illegal products and their buyers, which is also constantly monitored by legal authorities. As one common way for evasion, the merchants and buyers together create a vocabulary of jargons (called “black keywords” in this paper) to disguise the transaction (e.g., “smack” is one street name for “heroin” [1]).  Understanding black keywords is of great importance to track and disrupt the underground economy, but it is also prohibitively difficult: the investigators have to infiltrate the inner circle of criminals to learn their meanings, a task both risky and time- consuming. In this talk Prof. Duan  will introduce their attempt towards capturing and understanding the ever-changing black keywords. We investigated the underground business promoted through blackhat SEO (search engine optimization) and demonstrate that the black keywords targeted by the SEOers can be discovered through a fully automated approach. Together with Baidu, the leading search engine in China,  Prof. Duan’s team built a system called KDES (Keywords Detection and Expansion System), and applied it to the search results of Baidu. So far, they have already identified 478,879 black keywords which were clustered under 1,522 core words based on text similarity. They further extracted the information like emails, mobile phone numbers and instant messenger IDs from the pages and domains relevant to the underground business. Such information is helpful to understand the underground economy of China in particular.

Bio:
Dr. Haixin Duan is a professor in the Institute for Network Science and Cyberspace at Tsinghua University. He was once a visiting scholar at UC Berkeley and a senior scientist in International Computer Science Institute(ICSI).  Professor Duan focuses his research on network security, including security of network protocols, intrusion detection and underground economy detection. His research results were published in top security conferences like Security & Privacy, USENIX Security, CCS and NDSS. One of his research won Distinguished Paper Award of NDSS 2016. Prof. Duan won the  Excellence Talent Award for Cybersecurity (one of ten awardees from both academia and industry in China).