Program Analysis - Meanwhile, in Academia

POPKORN: Popping Windows Kernel Drivers At Scale

pr0v3rbs/FirmAE: Towards Large-Scale Emulation of IoT Firmware for Dynamic Analysis

Web Developers, Beware of the Tarpits for SAST in Your Code - Luca Compagna & Feras Al Kassar - YouTube

Quantifiable Quality The New Standard of Secure Code - Matias Madou - YouTube

ast-grep/ast-grep: ⚡A fast and easy tool for code searching, linting, rewriting at large scale. Written in Rust

0x4ndy/clif https://twitter.com/0x4ndy

trailofbits/siderophile: Find the ideal fuzz targets in a Rust codebase

Learn how to fuzz like a pro: Introduction to fuzzing - YouTube

microsoft/pyright: Static type checker for Python

Fuzzing101 with LibAFL - Part I: Fuzzing Xpdf

Z3 Solver Simplifying String Decryption - Custom Tools, Reverse Engineering, and Threat Research

An introduction to Datalog

Symbolic testing with Halmos: Leveraging existing tests for formal verification - a16z crypto

A Journey into Fuzzing WebAssembly Virtual Machine [BHUSA 2022] - YouTube

Hermit: Deterministic Linux for Controlled Testing and Software Bug-finding

Literature review on the benefits of static types https://danluu.com/empirical-pl/

Hyperpom: An Apple Silicon Fuzzer for 64-bit ARM Binaries - Impalabs Blog

A Compiler Writing Playground

A quick comparison of Security Static Code Analyzers for C# - DEV Community 👩‍💻👨‍💻

Learn how to fuzz like a pro: Fuzzing Arithmetics - YouTube

[2211.02652] AntFuzzer: A Grey-Box Fuzzing Framework for EOSIO Smart Contracts

crytic/amarna: Amarna is a static-analyzer and linter for the Cairo programming language.

Talk: Finding High-Value Vulnerabilities with Program Analysis - YouTube

Use Cases - ArchUnit

Fuzzing Solidity Smart Contracts with Echidna: Die-Hard Level Tips | by Cia Officer | Oct, 2022 | Pessimistic Security https://twitter.com/officer_cia

Verifying distributed systems with Isabelle/HOL — Martin Kleppmann’s blog

The Little Typer

Hacking TMNF: Part 1 - Fuzzing the game server | bricked.tech Hacking TMNF: Part 2 - Exploiting a blind format string | bricked.tech

A two-part series on fuzzing and exploiting the Trackmania Nations Forever server. The first part covers how the author configured a grammar fuzzer with LibAFL and Nautilus to to fuzz the game server, while the second part focuses on the exploitation of a Blind Format String in the error logger and how the author achieved remote code execution.

IDE Support for Cloud-Based Static Analyses

Abstract: We present a user study with developers at Amazon Web Services on their expectations of IDE support for cloud-based static analyses. The paper was originally presented at ESEC/FSE 2021. Many companies are providing Static Application Security Testing (SAST) tools as a service. These tools fit well into CI/CD, because CI/CD allows time for deep static analyses on large code bases and prevents vulnerabilities in the early stages of the development lifecycle. In CI/CD, the SAST tools usually run in the cloud and provide findings via a web interface. Recent studies show that developers prefer seeing the findings of these tools directly in their IDEs. Most tools with IDE integration run lightweight static analyses and can give feedback at coding time, but SAST tools take longer to run and usually are not able to do so. Can developers interact directly with a cloud-based SAST tool that is typically used in CI/CD through their IDE? We conducted a user study to explore how such IDE support should be designed. Through this study we identified the key design elements expected by developers and investigated whether an IDE solution fits better into developers’ workflow in comparison to a web-based solution.

https://dl.gi.de/bitstream/handle/20.500.12116/37971/A1-19.pdf?sequence=1&isAllowed=y

The five-minute feedback fix

The Little Prover

Fuzzing101 with LibAFL - Part I: Fuzzing Xpdf

Finding Prototype Pollution gadgets with CodeQL :: jorgectf — blog

Find and replace with type information · Comby

(19) NCC Group Research & Technology on Twitter: “As a bonus the team discusses how they used CodeQL not to find vulnerable code but to find exploitation primitives.. This technique was inspired by @mmolgtm and their 2019 and 2021 work leveraging CodeQL in these posts: https://t.co/RoEqFN91zH https://t.co/uXxRenfToO https://t.co/X0OSqvQYFs” / Twitter Shared by Kurt Boberg

Maat

Copilot: home

Do You Speak My Language? Make Static Analysis Engines Understand Each Other - YouTube

https://github.com/openrewrite/rewrite-java-security/tree/main/src/main/java/org/openrewrite/java/security/marshalling

Automated reasoning at Amazon: a conversation - Amazon Science

Fuzz Map

Using Graphs to Search for Code · Nick Gregory Compare Go graph query vs Semgrep search. Also is he counting the graph building time? There is a meta point here around ease of use, who can use it, speed, performance, flexibility/customizability, maintainability.

How to Patch Requests to Have a Default Timeout - Adam Johnson

sarsko/CreuSAT: CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

securing.dev - Static Analysis
A series of blog posts by GitHub Code Scanning Architect Keith Hoodlet which give an overview of three approaches: traditional static code analysis, binary static analysis, and “comprehensive static analysis.”

“Comprehensive static analysis” meaning tools that integrate into build processes to more precisely map data flows.

I’m always excited to see more people writing about static analysis, and overall I think the posts provide some nice background and context, but to be honest I disagree with some of the characterizations.

1) Keith seems to imply that traditional SAST tools can’t do dataflow analysis. I interned at Fortify and have helped customers use Checkmarx, and I know they can. Yes they are noisy, but for other reasons.

2) I expected more discussion of fundamental trade-offs when you’re doing static analysis, for example, soundness vs completeness, speed/memory/precision trade-offs, Rice’s theorem, etc.

3) Keith hones in on “local” vs “remote” sources as major sources of false positives in practice, and he’s dead right. Many tools by default consider “local” sources (e.g. properties files, environment variables, command-line args) as potentially dangerous sources of attacker input. 99% of the time this is not the case, and you want to ignore these, as if an attacker is already on your server you have bigger problems than SQL injection via environment variable or whatever.

However, TODO

4) There’s no discussion of customizability as one of the key selling points of a static analysis tool. In my (and many companies’) experience, code base or org-specific checks are some of the highest impact/signal/ROI checks. They’re usually business logic bugs or authentication or authorization bypasses, which out-of-the-box rules will almost never find (for any tool), because they generally don’t understand your business context. See Figma’s Devdatta Akhawe’s excellent Modern Static Analysis: how the best tools empower creativity.

5) Lastly, I’d argue that trying to “find all the bugs” is Security 1.0, regardless of how advanced your tooling is (static, dynamic, whatever). Secure guardrails and security engineering are Security 2.0 or higher.

Alright, well this is much more than I was planning to write 🤷

Anywho, I enjoyed reading these posts, and just to be clear, I think CodeQL is a powerful tool written by some very smart people.

Thanks for sharing these Keith, anyone writing about program analysis has a warm place my heart ✊

For CSA, plugging into the build process means that it is able determine how remote sources will sink within the application - and what (if any) sanitization steps take place throughout that process. This allows for analysis to accurately distinguish between sources that can be remotely exploited, as opposed to locally sourced exploits for which the underlying system would need to be compromised first (or a malicious developer would need to introduce attacks in properties files / environment variables et cetera).

The detailed mapping of an application’s data flows - and distinguishing between local vs. remote sources - is ultimately what differentiates Comprehensive Static Analysis from other solutions in this space.

While not as slow as Binary Static Analysis, CSA tools will be slower than traditional Static Code Analysis. Security teams rightly perceive this as adding friction to the development process, but often lose sight of the fact that producing more accurate findings far outweighs the small amount of additional time it takes to complete a security scan.

Since Comprehensive Static Analysis (CSA) is performed by accessing both the source code and build process, it is able to compile an accurate data flow map of the application - and therefore distinguish between Local and Remote sources.

Mutation testing offers a novel, automated system for comparing static analysis tools

in this paper by Alex Groce, Josselin Feist, Gustavo Grieco, and others. Alongside analyzers for Python and Java, they reviewed the efficacy of Solidity analyzers (including Slither) with mutation testing and identified opportunities for three new detectors, one of which has already caught issues in real code audits since then (divide-before-multiply).

Ghidra2CPG: From Graph Queries to Vulnerabilities in Binary Code
ShiftLeft’s C, Fabian Yamaguchi, and Niko discuss

SOK: On the Analysis of Web Browser Security

https://twitter.com/michael_w_hicks/status/1474093197571895306 This 2013 paper by @khooyp (now at @MathWorks ) exploring a declarative interface for time travel debugging did not quite get the love it deserved. With a little more development this stuff could be game changing. https://drum.lib.umd.edu/bitstream/handle/1903/14406/CS-TR-5021.pdf

https://twitter.com/aurelsec/status/1351600286943633409

Very proud and excited to open-source Yin-Yang for testing SMT solvers on GitHub at https://lnkd.in/dvp8c77. It is an umbrella release with both Semantic Fusion and OpFuzz from our PLDI and OOPSLA papers. The tool has already found 1,000+ bugs in Z3 and CVC4. Please check it out!

https://testsmt.github.io/ https://github.com/testsmt/yinyang