-
Macaw: A Machine Code Toolbox for the Busy Binary Analyst
Authors:
Ryan G. Scott,
Brett Boston,
Benjamin Davis,
Iavor Diatchki,
Mike Dodds,
Joe Hendrix,
Daniel Matichuk,
Kevin Quick,
Tristan Ravitch,
Valentin Robert,
Benjamin Selfridge,
Andrei Stefănescu,
Daniel Wagner,
Simon Winwood
Abstract:
When attempting to understand the behavior of an executable, a binary analyst can make use of many different techniques. These include program slicing, dynamic instrumentation, binary-level rewriting, symbolic execution, and formal verification, all of which can uncover insights into how a piece of machine code behaves. As a result, there is no one-size-fits-all binary analysis tool, so a binary a…
▽ More
When attempting to understand the behavior of an executable, a binary analyst can make use of many different techniques. These include program slicing, dynamic instrumentation, binary-level rewriting, symbolic execution, and formal verification, all of which can uncover insights into how a piece of machine code behaves. As a result, there is no one-size-fits-all binary analysis tool, so a binary analysis researcher will often combine several different tools. Sometimes, a researcher will even need to design new tools to study problems that existing frameworks are not well equipped to handle. Designing such tools from complete scratch is rarely time- or cost-effective, however, given the scale and complexity of modern ISAs.
We present Macaw, a modular framework that makes it possible to rapidly build reliable binary analysis tools across a range of use cases. Statically typed functional programming techniques are used pervasively throughout Macaw -- these range from using functional optimization passes to encoding tricky architectural invariants at the type level to statically check correctness properties. The level of assurance that functional programming ideas afford us allow us to iterate rapidly on Macaw while still having confidence that the underlying semantics are correct. Over a decade of development, we have used Macaw to support an industrial research team in building tools for machine code-related tasks. As such, the name 'Macaw' refers not just to the framework, but also a suite of tools that are built on top of it. We describe Macaw in depth and describe the different static and dynamic analyses that it performs, many powered by an SMT-based symbolic execution engine. We put a particular focus on interoperability between machine code and higher-level languages, including binary lifting from x86 to LLVM, as well verifying the correctness of mixed C and assembly code.
△ Less
Submitted 18 February, 2025; v1 submitted 8 July, 2024;
originally announced July 2024.
-
EvoBA: An Evolution Strategy as a Strong Baseline forBlack-Box Adversarial Attacks
Authors:
Andrei Ilie,
Marius Popescu,
Alin Stefanescu
Abstract:
Recent work has shown how easily white-box adversarial attacks can be applied to state-of-the-art image classifiers. However, real-life scenarios resemble more the black-box adversarial conditions, lacking transparency and usually imposing natural, hard constraints on the query budget.
We propose $\textbf{EvoBA}$, a black-box adversarial attack based on a surprisingly simple evolutionary search…
▽ More
Recent work has shown how easily white-box adversarial attacks can be applied to state-of-the-art image classifiers. However, real-life scenarios resemble more the black-box adversarial conditions, lacking transparency and usually imposing natural, hard constraints on the query budget.
We propose $\textbf{EvoBA}$, a black-box adversarial attack based on a surprisingly simple evolutionary search strategy. $\textbf{EvoBA}$ is query-efficient, minimizes $L_0$ adversarial perturbations, and does not require any form of training.
$\textbf{EvoBA}$ shows efficiency and efficacy through results that are in line with much more complex state-of-the-art black-box attacks such as $\textbf{AutoZOOM}$. It is more query-efficient than $\textbf{SimBA}$, a simple and powerful baseline black-box attack, and has a similar level of complexity. Therefore, we propose it both as a new strong baseline for black-box adversarial attacks and as a fast and general tool for gaining empirical insight into how robust image classifiers are with respect to $L_0$ adversarial perturbations.
There exist fast and reliable $L_2$ black-box attacks, such as $\textbf{SimBA}$, and $L_{\infty}$ black-box attacks, such as $\textbf{DeepSearch}$. We propose $\textbf{EvoBA}$ as a query-efficient $L_0$ black-box adversarial attack which, together with the aforementioned methods, can serve as a generic tool to assess the empirical robustness of image classifiers. The main advantages of such methods are that they run fast, are query-efficient, and can easily be integrated in image classifiers development pipelines.
While our attack minimises the $L_0$ adversarial perturbation, we also report $L_2$, and notice that we compare favorably to the state-of-the-art $L_2$ black-box attack, $\textbf{AutoZOOM}$, and of the $L_2$ strong baseline, $\textbf{SimBA}$.
△ Less
Submitted 12 July, 2021;
originally announced July 2021.
-
Identity Management on Blockchain -- Privacy and Security Aspects
Authors:
Andreea-Elena Panait,
Ruxandra F. Olimid,
Alin Stefanescu
Abstract:
In the last years, identity management solutions on blockchain were proposed as a possible solution to the digital identity management problem. However, they are still at an early stage and further research needs to be done to conclude whether identity systems could benefit from the use of blockchain or not. Motivated by this, we investigate identity management solutions on blockchain intending to…
▽ More
In the last years, identity management solutions on blockchain were proposed as a possible solution to the digital identity management problem. However, they are still at an early stage and further research needs to be done to conclude whether identity systems could benefit from the use of blockchain or not. Motivated by this, we investigate identity management solutions on blockchain intending to give the reader an overview of the current status and provide a better understanding of the pros and cons of using such solutions. We conduct an analysis on ten of the most known implementations, with a focus on privacy and security aspects. Finally, we identify existing challenges and give new directions for research.
△ Less
Submitted 27 April, 2020;
originally announced April 2020.
-
All-Path Reachability Logic
Authors:
Andrei Stefanescu,
Stefan Ciobaca,
Radu Mereuta,
Brandon Moore,
Traian Florin Serbanuta,
Grigore Rosu
Abstract:
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof…
▽ More
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language. The soundness has also been mechanized in Coq. This approach is implemented in a tool for semantics-based verification as part of the K framework (http://kframework.org)
△ Less
Submitted 29 April, 2019; v1 submitted 25 October, 2018;
originally announced October 2018.
-
A Constructor-Based Reachability Logic for Rewrite Theories
Authors:
Stephen Skeirik,
Andrei Stefanescu,
José Meseguer
Abstract:
Reachability logic has been applied to $\mathbb{K}$ rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. The logic's automation is increased by means of constructor-based semantic unif…
▽ More
Reachability logic has been applied to $\mathbb{K}$ rewrite-rule-based language definitions as a language-generic logic of programs. To be able to verify not just code but also distributed system designs, a new rewrite-theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. The logic's automation is increased by means of constructor-based semantic unification, matching, and satisfiability procedures. New methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new proof methods are presented.
△ Less
Submitted 14 September, 2017;
originally announced September 2017.
