RRecherchily
← Back to projects
ActiveSeptember 2025

Formal Verification of Open-Source Software Packages via Hybrid Static Analysis and Machine Learning Classification

Open-source package registries (PyPI, npm) have become major attack vectors through malicious code injection in transitive dependencies. This project develops a hybrid pipeline combining static data-flow analysis (taint analysis) and an ML classifier trained on signatures of known malicious packages to automatically detect suspicious behaviors before publication.

Formal verificationStatic analysisSupply chainSoftware security

Team

AM
Abdelhamid MASSERITI
Research Director
KT
Karim TOUATI
Researcher

Methodology

  1. Build a corpus of 500 documented malicious packages (Backstabber's Knife Collection, MalOSS) and 5,000 benign packages for classifier training.
  2. Implement an inter-procedural static analyzer based on control-flow graphs (CFG) and data-flow graphs (DFG) for Python and JavaScript.
  3. Train a Graph Neural Network (GNN) model on extracted graph representations, with augmentation through synthetic mutations.
  4. Evaluate on a separate test set of 200 recently flagged packages, comparing with existing tools (Bandit, Semgrep, Socket).

Evaluation metrics

  • Detection rate (recall) on malicious packages — target > 92%.
  • False positive rate — target < 5% on benign packages.
  • Average analysis time per package — target < 30 seconds.

Budget

$800 in GPU compute credits (Google Cloud) for GNN training, $200 for CI/CD infrastructure of the analysis pipeline.

Expected deliverables

  • Open-source package analysis tool publishable as a GitHub Action / npm pre-publish hook.
  • Annotated dataset of package flow graphs (malicious and benign) on Hugging Face.
  • Paper submitted to ICSE 2027 (International Conference on Software Engineering).
← Back to projects