Differ: Tool for testing and validating transformed programs

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Our great sponsors
  • WorkOS - The modern identity platform for B2B SaaS
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • SaaSHub - Software Alternatives and Reviews
  • x509-limbo

    A suite of testvectors for X.509 certificate path validation and tools for building them

  • Differential fuzzing is woefully underutilized -- our experience is that it consistently[1] finds[2] bugs that "traditional" fuzzing techniques struggle to discover, and that the primary obstacles to its adoption are harness and orchestration complexity. DIFFER goes a long way towards overcoming those obstacles!

    (FD: My company.)

    [1]: https://github.com/trailofbits/mishegos

    [2]: https://x509-limbo.com/

  • mishegos

    A differential fuzzer for x86 decoders

  • Differential fuzzing is woefully underutilized -- our experience is that it consistently[1] finds[2] bugs that "traditional" fuzzing techniques struggle to discover, and that the primary obstacles to its adoption are harness and orchestration complexity. DIFFER goes a long way towards overcoming those obstacles!

    (FD: My company.)

    [1]: https://github.com/trailofbits/mishegos

    [2]: https://x509-limbo.com/

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo
  • osv

    Discontinued Open source vulnerability DB and triage service. [Moved to: https://github.com/google/osv.dev] (by google)

  • https://google.github.io/clusterfuzz/setting-up-fuzzing/libf...

    > OSS-Fuzz runs CloudFuzz[Lite?] for many open source repos and feeds OSV OpenSSF Vulnerability Format: https://github.com/google/osv#current-data-sources

    .

    Google/syzkaller https://github.com/google/syzkaller :

    >> syzkaller is an unsupervised coverage-guided kernel fuzzer. Supported OSes: Akaros, FreeBSD, Fuchsia, gVisor, Linux, NetBSD, OpenBSD, Windows

    .

    ghidra-patchdiff-correlator:

  • syzkaller

    syzkaller is an unsupervised coverage-guided kernel fuzzer

  • https://google.github.io/clusterfuzz/setting-up-fuzzing/libf...

    > OSS-Fuzz runs CloudFuzz[Lite?] for many open source repos and feeds OSV OpenSSF Vulnerability Format: https://github.com/google/osv#current-data-sources

    .

    Google/syzkaller https://github.com/google/syzkaller :

    >> syzkaller is an unsupervised coverage-guided kernel fuzzer. Supported OSes: Akaros, FreeBSD, Fuchsia, gVisor, Linux, NetBSD, OpenBSD, Windows

    .

    ghidra-patchdiff-correlator:

  • Regshot

    Regshot is a small, free and open-source registry compare utility that allows you to quickly take a snapshot of your registry and then compare it with a second one - done after doing system changes or installing a new software product

  • CompCert

    The CompCert formally-verified C compiler

  • A big problem is that proving that transformations preserve semantics is very hard. Formal methods has huge potential and I believe it will be a big part of the future, but it hasn't become mainstream yet. Probably a big reason why is that right now it's simply not practical: the things you can prove are much more limited than the things you can do, and it's a lot less work to just create a large testsuite.

    Example: CompCert (https://compcert.org/), a formally-verified compiler AKA formally-verified sequence of semantics-preserving transformations from C code to Assembly. It's a great accomplishment, but few people are actually compiling their code with CompCert. Because GCC and LLVM are much faster[1], and have been used so widely that >99.9% of code is going to be compiled correctly, especially code which isn't doing anything extremely weird.

    But as articles like this show, no matter how large a testsuite there may always be bugs, tests will never provide the kind of guarantees formal verification does.

    [1] From CompCert, "Performance of the generated code is decent but not outstanding: on PowerPC, about 90% of the performance of GCC version 4 at optimization level 1"

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts