SaTC: CORE: Medium: Collaborative: Effective Formal Reasoning for Mobile Malware

自十年前问世以来，智能手机已成为我们数字生活的支柱，存储着从医疗和银行数据到我们整个电子通信历史的安全敏感信息。由于我们在日常生活中越来越依赖移动应用程序，移动恶意软件样本的数量和复杂性都在稳步增加。这个项目的影响是让用户和组织更容易识别恶意应用程序，从而防止全球各地的人们成为移动恶意软件的受害者。该项目的新颖之处在于开发先进的程序分析和自然语言处理技术，以识别不同恶意软件家族的显著特征，并使用它们来检测以前未知的恶意软件实例。这个项目的技术工作集中在几个方面。首先是“反协议”的匹配，它是表征恶意行为的抽象事件序列。调查人员将探索识别反协议的方法，并将其与应用程序进行精确和近似的匹配。其次，由于恶意软件实例通常通过行为混淆来伪装自己，因此该项目将研究新技术，以精确和准确地推断被混淆的移动应用程序。最后，检测恶意软件可能需要识别与可能用自然语言指定的行为不一致的地方。调查人员开发了一种技术，用于描述程序所声明的操作与其正式分析的指纹之间的一致性，以便发现意想不到的，可能是恶意的行为。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Since their inception a decade ago, smartphones have become the pillars of our digital life, storing security-sensitive information ranging from medical and banking data to our entire electronic communication history. Due to our increasing reliance on mobile applications in daily life, there has been a steady increase in both the number and sophistication of mobile malware samples. This project's impacts are to make it easier for users and organizations to identify malicious applications and thereby prevent people from around the globe from becoming victims of mobile malware. The project's novelties are to develop advanced program analysis and natural language processing techniques to identify salient characteristics of different malware families and use them to detect previously unknown malware instances.This project's technical effort is focused on several fronts. The first is matching of "anti-protocols", which are sequences of abstract events characterizing malicious behavior. The investigators will explore approaches for identifying anti-protocols and matching them both exactly and approximately against apps. Second, since malware instances typically disguise themselves through behavioral obfuscation, the project will investigate new techniques for reasoning precisely and accurately about obfuscated mobile applications. Finally, detecting malware may require identifying inconsistencies with behavior that might be specified in natural language. The investigators develop techniques for characterizing the alignment between a program's stated operation and its formally-analyzed fingerprint in order to spot unexpected, possibly malicious behavior.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.