Growing A Test Corpus with Bonsai Fuzzing @ICSE'21

For generating synthesization automatically based on the ChocoPy dialect which I'm in great need of, the author of ChocoPy published their tricky counterpart to C-smith/ Fuzzy Grammer Generator called Bonsal Fuzzing.

Problems and Pair Review

Instead of Fuzz-then-reduce method, the corpus bottom up generation is already concise. enough and can touch much of the corner test cases.

  1. Bounded Exhaustive Testing: input of bounded size are generated systematically but not enumerated exhaustively
  2. So enumerate the k-path with the grammar.
  3. JPF-SE explores the space of program paths, for bounding the size of a comprehensive test suite that covers a diverse set of program paths
  4. different kind of strategies of fuzzing: Coverage-Guided Fuzzing, Specialized Compiler Fuzing, Grammar-based, Semantic Fuzzing(Zest)
  5. Test-Case Reduction by Hieachical delta debugging

Implementation

  1. Bounded Grammar Fuzzers: Bound iteration by idens, items, depths number.

  2. Coverage-Guided Bounded Grammar Fuzzing


    The lattice of coverage-guided size-bounded grammar-based fuzzers $F_{m,n,d}$, ordered by three size bounds on the syntax of the test cases they produce: number of unique identifiers m, maximum sequence length n, and maximum nesting depth d.

Test cases flow along directed edges: the inputs generated by each fuzzer are used as the seed inputs to its successors. The result of bonsai fuzzing is the corpus produced by the top-most element.

  1. Bonsai fuzzing with extended lattice


Encountering `::signbit` stuff not passing to `math.h` in MacOS 12.4

TL;DR

/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:317:9: error: no member named 'signbit' in the global namespace
using ::signbit;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:318:9: error: no member named 'fpclassify' in the global namespace
using ::fpclassify;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:319:9: error: no member named 'isfinite' in the global namespace
using ::isfinite;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:320:9: error: no member named 'isinf' in the global namespace
using ::isinf;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:321:9: error: no member named 'isnan' in the global namespace
using ::isnan;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:322:9: error: no member named 'isnormal' in the global namespace
using ::isnormal;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:323:9: error: no member named 'isgreater' in the global namespace
using ::isgreater;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:324:9: error: no member named 'isgreaterequal' in the global namespace
using ::isgreaterequal;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:325:9: error: no member named 'isless' in the global namespace
using ::isless;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:326:9: error: no member named 'islessequal' in the global namespace
using ::islessequal;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:327:9: error: no member named 'islessgreater' in the global namespace
using ::islessgreater;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:328:9: error: no member named 'isunordered' in the global namespace
using ::isunordered;
      ~~^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/cmath:329:9: error: no member named 'isunordered' in the global namespace
using ::isunordered;
      ~~^

When I was compiling LLVM recently I found this, it may be because my CommandLineTool is outdated as described in stackoverflow. And I reinstalled it with following code added.

using ::signbit _LIBCPP_USING_IF_EXISTS;
using ::fpclassify _LIBCPP_USING_IF_EXISTS;
using ::isfinite _LIBCPP_USING_IF_EXISTS;
using ::isinf _LIBCPP_USING_IF_EXISTS;
using ::isnan _LIBCPP_USING_IF_EXISTS;
using ::isnormal _LIBCPP_USING_IF_EXISTS;
using ::isgreater _LIBCPP_USING_IF_EXISTS;
using ::isgreaterequal _LIBCPP_USING_IF_EXISTS;
using ::isless _LIBCPP_USING_IF_EXISTS;
using ::islessequal _LIBCPP_USING_IF_EXISTS;
using ::islessgreater _LIBCPP_USING_IF_EXISTS;
using ::isunordered _LIBCPP_USING_IF_EXISTS;
using ::isunordered _LIBCPP_USING_IF_EXISTS;

_LIBCPP_USING_IF_EXISTS is defined as # define _LIBCPP_USING_IF_EXISTS __attribute__((using_if_exists)), simply pass if no defined in the global namespace.

Then the following code output error

using _Lim = numeric_limits<_IntT>;

add another header in

#include <limits>

Then comes to the std::isnan using bypassing no definition error in llvm/lib/Support/NativeFormatting.cpp.

error: expected unqualified-id for std::isnan(N)

just drop the std::

The full formula for riscv-rvv-llvm is located in https://github.com/victoryang00/homebrew-riscv, if anything above happens, do as the above specifies.

[Program Analysis] CHA Analysis in Soot

source

Helper Class

CHACallNode

I use a Node to record the caller callee and which invoke method the Call node is calling. The invoke method is recorded in an integer which is the offset for the following enum

enum InvokeMorphism {
    InterfaceInvokeExpr,
    VirtualInvokeExpr,
    SpecialInvokeExpr,
    StaticInvokeExpr,
    JStaticInvokeExpr,
    JSpecialInvokeExpr,
    JVirtualInvokeExpr,
    JInterfaceInvokeExpr
}

The toString method are overridden for linting the line and the <CHAInput: void main(java.lang.String[])>-><CHAInput: int addOne(int)>.

ReachableMethods

This method maintains Set<SootMethod>. The toString method to linting the line Reachable.

CHAAnalysis

This class maintains the CallerCalleeMap for the latter use by virtual calls, the cha_class contains the information of Class FastHierachy, entries will store the init entries and will put it into the worklist queue, it will add to worklist if the function is invoked and reachable from the stand view from method main. unitSootMethodMap is to store the unit method relations and will init in the first place and will be used in the call printing.

UCLID5: Integrating Modeling, Verification, Synthesis, and Learning

When I was browsing keystones‘ paper, they are applying a verification model called UCLID5, a new software toolkit based on z3 written in scala for the formal modeling, specification, verification, and synthesis of computational systems. The augmented efforts are merely making architectural implementations like NAPOT/S mode world change/exceptions in pmp reg mapping policy to Hoare logic and do the verification. To a greater extent, the Y86-64 introduced in CSAPP is verified by UCLID5, too.

The Goals

  1. Enabling modular modeling of finite and infinite-state transition systems across a range of concurrency models and background logical theories.
  2. Performing a highly-automated, compositional verification of a diverse class of specifications, including pre/post conditions, assertions, invariant, LTL, refinement and hyperproperties
  3. Integrating modeling and verification with algorithmic synthesis and learning.

threat models

SRE

Heartbleed-like attack, side channels, and Meltdown/Spectre are also cast a lot on SGX/TEE. Stuff like secure remote extensions using trusted platforms is introduced. They formalized the enclave platform and made remote execution trustworthy.

embodying enclave and adversary






UCLID5 verifier


Modules, like LLVM, serve as the unit of re-use when declaring commonly used types, symbolic constants, and uninterpreted functions. The module uses uninterpreted functions to model instruction decoding (inst2op, inst2reg0 etc.) and instruction execution (aluOp and nextPC). Further, the register file index type (regindex_t) and the address type (addr_t) are both uninterpreted types. This abstraction is sufficient to model all kinds of CPU implementation.

Structure of the CPU Model:

  1. Module common: serves as top-level type definition.
  2. Module cpu: defining the initial sate like reg/pc/imem/dmem, types are mode_t(isolated/normal) word_t addr_t(a range of addresses between isolated_rng_lo and isolated_rng_hi) init/next/exec_inst defines the transition system.
  3. Module main: the environmental assumptions for the verification and contains a proof script that proves, via induction, a 2-safety integrity property for the CPU module.

Other features

  1. Term-Level Abstraction: In term-level abstraction, concrete functions or functional blocks are replaced by uninterpreted functions or partially-interpreted functions. Concrete low-level data types such as Booleans, bit-vectors, and finite-precision integers are abstracted away by uninterpreted symbols or more abstract data types (such as the unbounded integers).
  2. Blending Sequential and Concurrent System Modeling:
  3. Diversity in Specification
    1. Procedure specifications.
      1. Invariant
      2. while
      3. assume
      4. assert
    2. LTL
    3. Hyperproperties(k-safety): composing k copies of the system together and specifying a safety property on the resulting composition
  4. Modularity in Modeling and Specification
  5. Counterexample Generation
  6. Modular Proof Scripting

More for extended reading

  1. https://www.hillelwayne.com/post/hyperproperties/https://www.cs.unc.edu/~csturton/courses/verifiedsec/lecturenotessp17/notes_lbarnett.pdf

[Program Analysis] Soundiness and soundness

In defense to a situation where no program analysis in the program is soundness, so given term soundness for that program claims that they can cover most cases.

Reflection in Java

First on Java reflection: Class + Method + Field Metaobject

  1. One solution: String Constant analysis + Pointer Analysis
  2. List and Array propagation

JNI Call

  1. One Solution: Transcode from C to Java
  2. scanning on the binary

[A Primer on Memory Persistency] Persistent Memories阅读笔记

本篇是《A Primer on Memory Persistency》这本书的中文阅读笔记,会整理出我认为重要的部分。当年看《A Primer on Memory Consistency and Cache Coherence》的时候,被其对内存的描述惊艳到了,也是我对内存提起兴趣的最重要的原因。上CA2的时候对这几本书翻了又翻。

Continue reading "[A Primer on Memory Persistency] Persistent Memories阅读笔记"