Publications (15)
Optimizing Datalog for the GPU
Yihao Sun, Ahmedur Rahman Shovon, Thomas Gilray +2
Modern Datalog engines (e.g., LogicBlox, Soufflé, ddlog) enable their users to write declarative queries which compute recursive deductions over extensional facts, leaving high-pe…
Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
Kristopher Micinski, Jonathan Fetter-Degges, Jinseong Jeon +2
Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to prote…
Racets: Faceted Execution in Racket
Kristopher Micinski, Zhanpeng Wang, Thomas Gilray
Faceted Execution is a linguistic paradigm for dynamic information-flow control. Under faceted execution, secure program data is represented by faceted values: decision trees that…
Datalog with First-Class Facts
Thomas Gilray, Arash Sahebolamri, Yihao Sun +3
Datalog is a popular logic programming language for deductive reasoning tasks in a wide array of applications, including business analytics, program analysis, and ontological reaso…
Terascale Query Processing in the Browser: Rethinking GPU Acceleration
Jiaxin Lu, Landon Dyken, Yihao Sun +3
Recursive query computation, central to graph algorithms and relational databases, demands GPU acceleration due to its inherent computational intensity. While substantial prior wor…
Scaling Worst-Case Optimal Datalog to GPUs
Yihao Sun, Kunting Qi, Thomas Gilray +2
Datalog is a declarative logic-programming language used for complex analytic reasoning workloads such as program analysis and graph analytics. Datalog's popularity is due to its u…
Column-Oriented Datalog on the GPU
Yihao Sun, Sidharth Kumar, Thomas Gilray +1
Datalog is a logic programming language widely used in knowledge representation and reasoning (KRR), program analysis, and social media mining due to its expressiveness and high pe…
An Observational Investigation of Reverse Engineers' Processes
Daniel Votipka, Seth M. Rabin, Kristopher Micinski +2
Reverse engineering is a complex process essential to software-security tasks such as vulnerability discovery and malware analysis. Significant research and engineering effort has…
Is Function Similarity Over-Engineered? Building a Benchmark
Rebecca Saul, Chang Liu, Noah Fleischmann +4
Binary analysis is a core component of many critical security tasks, including reverse engineering, malware analysis, and vulnerability detection. Manual analysis is often time-con…
Higher-Order, Data-Parallel Structured Deduction
Thomas Gilray, Arash Sahebolamri, Sidharth Kumar +1
State-of-the-art Datalog engines include expressive features such as ADTs (structured heap values), stratified aggregation and negation, various primitive operations, and the oppor…
Declarative Demand-Driven Reverse Engineering
Yihao Sun, Jeffrey Ching, Kristopher Micinski
Binary reverse engineering is a challenging task because it often necessitates reasoning using both domain-specific knowledge (e.g., understanding entrypoint idioms common to an AB…
Assemblage: Automatic Binary Dataset Construction for Machine Learning
Chang Liu, Rebecca Saul, Yihao Sun +5
Binary code is pervasive, and binary analysis is a key task in reverse engineering, malware classification, and vulnerability discovery. Unfortunately, while there exist large corp…
ASSEMBLAGE-DEEPHISTORY: A Cross-Build Binary Dataset with Temporal Coverage
Chang Liu, Noah Fleischmann, Nicolò Altamura +3
Existing binary corpora typically capture only one or two axes of binary variation: they either provide cross-compiler builds without a temporal axis, or CVE labels for single-buil…
So You Want to Analyze Scheme Programs With Datalog?
Davis Ross Silverman, Yihao Sun, Kristopher Micinski +1
Static analysis approximates the results of a program by examining only its syntax. For example, control-flow analysis (CFA) determines which syntactic lambdas (for functional lang…
Superset Decompilation
Chang Liu, Yihao Sun, Thomas Gilray +1
Reverse engineering tools remain monolithic and imperative compared to the advancement of modern compiler architectures: analyses are tied to a single mutable representation, makin…