SHF

group_project

Visible to the public SHF: Small: Reverse Engineering Obfuscated Executables

Submitted by debray on Sun, 04/22/2018 - 3:46pm

Computer malware codes are usually heavily obfuscated via a variety of techniques that make it difficult to understand the logic of the code. Existing tools for malware analysis do not provide much support for automatically removing such obfuscations, which therefore requires a great deal of time-consuming manual intervention. This project aims to develop techniques and tools to automate the identification and removal of obfuscation code from malware programs, focusing in particular on a class of obfuscations called "virtualization-based obfuscation".

Outcomes Report URL: 
https://www.research.gov/research-portal/appmanager/base/desktop?_nfpb=true&_win...
group_project

Visible to the public SHF: Small: Architectural Support for Security in the Many-core Age: Threats and Opportunities

Submitted by Dmitry Ponomarev on Tue, 03/13/2018 - 4:38pm

Modern multicore and manycore architectures have a number of new security threats. For example, shared microarchitecture components such as caches, core inter-connection networks, and memory controllers can be exploited for side-channel attacks or denial of service attacks. The evolution of workloads to exploit explicit parallelism will also likely lead to additional new threats. New forms of active viruses and trojans that reside on some cores and attempt to attack other applications are likely to arise.

Outcomes Report URL: 
https://www.research.gov/research-portal/appmanager/base/desktop?_nfpb=true&_win...
group_project

Visible to the public SHF: Medium: Collaborative Research: Building Critical Systems with Verifiable Properties Using Gate Level Analysis

Submitted by rck289 on Mon, 03/05/2018 - 5:28pm

Computer performance has doubled many times over during the past 40 years, but the very techniques used to achieve these performance gains have made it increasingly difficult to build systems that are provably safe, secure, or reliable. This fact significantly impedes progress in the development of our most safety-critical embedded systems such as those found in medical, avionic, automotive, and military systems.

Outcomes Report URL: 
https://www.research.gov/research-portal/appmanager/base/desktop?_nfpb=true&_win...
group_project

Visible to the public SHF: Medium: Collaborative Research: Formal Analysis and Synthesis of Multiagent Systems with Incentives

Submitted by Swarat Chaudhuri on Thu, 02/08/2018 - 12:41am

The project develops automated methods for the tool-aided design and analysis of multi-agent systems with incentives. These systems are natural models for real-world situations in which collections of actors interact with one another in an autonomous and self-interested manner. For example, such a system can model a set of software agents that participate in an internet-based protocol, such as an advertisement auction or crypto currency; a collection of robots that share physical or digital infrastructure; or a set of cells that participate in an evolutionary process.

group_project

Visible to the public  SHF: Small: Control-Flow and Data-Flow Analysis of Android Software: Foundations and Applications

Submitted by Atanas Rountev on Wed, 02/07/2018 - 4:20pm

In recent years the growth in the number of computing devices has been driven primarily by smartphones and tablets. For such devices, Android is the dominant platform. The correctness, security, and performance of Android devices is of paramount importance for many millions of users. However, the scientific foundations for software analysis, verification, and transformation in this area are still very inadequate. The proposed work will significantly advance the state of the art in software analysis for Android.

group_project

Visible to the public SHF: Small: Refinement Types For Verified Web Frameworks and Applications

Submitted by Ranjit Jhala on Wed, 02/07/2018 - 3:31pm

Web applications play a crucial role in every aspect of our lives, including banking, commerce, education and healthcare and travel. Despite their importance and ubiquity, they remain notoriously hard to design, develop and deploy as they span several tiers and languages: an HTML/JavaScript client that runs on users' browsers, a central server that implements the application's logic in the "cloud" and a database that stores persistent user data. The goal of this research is to build upon recent advances in SMT-based software verification to develop reliable and secure web frameworks.

group_project

Visible to the public SHF: Small: Adapting VLSI Test Principles for VLSI Trust

Submitted by Ozgur Sinanoglu on Tue, 02/06/2018 - 4:52pm

If an Integrated Circuit (IC) is designed and fabricated in a foundry that is outside the direct control of the (fab-less) design house, reverse engineering, malicious circuit modification, and Intellectual Property (IP) piracy are all possible. An attacker, anywhere in this design flow, can reverse engineer the functionality of design, and steal and claim ownership of the IP. An untrustworthy IC foundry may overbuild ICs and sell the excess parts in the gray market.

group_project

Visible to the public SHF: Small: Inference and Checking of Context-sensitive Pluggable Types

Submitted by Ana Milanova on Tue, 02/06/2018 - 4:47pm

Pluggable types allow programmers to extend a language's type system to enhance program correctness and program security. Unfortunately, pluggable types require annotations in the program, and therefore, place a burden on programmers. This annotation burden is one reason why pluggable types have not been widely adopted in practice. This project will develop techniques that will allow programmers to realize the benefits of pluggable types without incurring the annotation burden. One concrete application (and thrust of the project) tackles security and privacy of Android apps.