BinTrimmer: Towards Static Binary Debloating Through Abstract Interpretation

Abstract

The increasing complexity of modern programs motivates software engineers to often rely on the support of third-party libraries. Although this practice allows application developers to achieve a compelling time-to-market, it often makes the final product bloated with conspicuous chunks of unused code. Other than making a program unnecessarily large, this dormant code could be leveraged by willful attackers to harm users. As a consequence, several techniques have been recently proposed to perform program debloating and remove (or secure) dead code from applications. However, state-of-the-art approaches are either based on unsound strategies, thus producing unreliable results, or pose too strict assumptions on the program itself.

In this work, we propose a novel abstract domain, called Signedness-Agnostic Strided Interval, which we use as the cornerstone to design a novel and sound static technique, based on abstract interpretation, to reliably perform program debloating. Throughout the paper, we detail the specifics of our approach and show its effectiveness and usefulness by implementing it in a tool, called BinTrimmer, to perform static program debloating on binaries.

Our evaluation shows that BinTrimmer can remove up to 65.6% of a library’s code and that our domain is, on average, 98% more precise than the related work.

A Signedness-Agnostic Strided Interval Operations

We provided our abstract domain with every mathematical and logical operation included in today architectures’ instruction sets. However, due to space constraints, we detail here only the or bitwise operation.

1.1 A.1 Bitwise or

To define a precise and sound bitwise or operation we leverage the unsigned version of Warren’s algorithm [42], which performs the or operation on classic non-wrapping ranges of values. Given two generic SASIs $r = s_r[a,b]w$ and $t = s_t[c,d]w$, the algorithm used to calculate the bitwise or operation is shown in Algorithm 2.

First, we split r and t on the south poles, thus avoiding any wrapping intervals (i.e., intervals might include the values $1^w$ and $0^w$). Then, for each u and v resulting from the split, we create a new SASI calculating its stride ($s_z$) and bounds (lb and ub) separately. For the stride, we retrieve the number of trailing zeros (function ntz) in the bit-vector representations of $s_u$ and $s_v$ both, and consider the minimum of them to set the stride $s_z$ (Lines 5 and 6). In fact, as the strides $s_u$ and $s_v$ have t low-order bits unset, all the values represented by the SASI resulting from $u\ |_w^{wr}\ v$ share the same t low-order bits. Therefore, the choice of a stride equal to $2^t$ is a sound choice (line 6). The value of these t-lower bits is $k = (e \& m) | (g \& m)$ (where $m = (1 \ll t) - 1$). On the other hand, the ($w - t$) high-order bits are handled by masking out the obtained t low-order bits and then applying unsigned version of Warren’s or algorithm to find the bounds for the SASI resulting from $u |_w v$ (from line 9 to 11). Finally, the SASI resulting from $r\ |_w\ t$ is obtained by applying the generalized join on the list of SASIs collected by applying the algorithm just explained. Since Warren’s algorithm employed is sound, the or operation is sound.