Boqin Qin

Boqin Qin

I received my B.S. and Ph.D. in BUPT, China. I was a visiting scholar in PennState, US, 2018-2019. Interested in program analysis and distributed systems.

招生广告

less than 1 minute read

Published:

中国科学院计算技术研究所处理器芯片全国重点实验室宋林海老师课题组招收硕士生、直博生

宋老师将要入职中科院计算所处理器芯片全国重点实验室担任研究员。回国之前，宋老师是美国宾州州立大学（Pennsylvania State University）终身教职副教授（tenured associate professor）。宋老师课题组的研究方向包括系统，安全，软件工程，和机器学习。课题组有几个正在进行的项目：1）利用Rust提高底层软件的安全性；2）利用大模型辅助形式化验证；3）大模型推理系统及Agent系统的安全。

宋老师的课题组每年都有高质量的顶级学术论文产出。博士生毕业去向包括Meta，天翼云，北京邮电大学，Fontbonne University。实习去向包括Meta，Google，Bytedance。本科生实习生获得了系统领域顶级会议sosp学生科研竞赛的银牌。实习生读博士去向包括Gatech, Wisc, UCSD。

中科院计算所是中国计算机科研的国家队，处理器芯片实验室是全球顶尖的体系结构研究机构，享有很高的学术声誉，孵化了多家千亿元的国产处理器芯片企业（如龙芯、寒武纪、海光等）。

宋老师的个人主页：https://songlh.github.io/

处理器芯片重点实验室介绍：http://www.ict.ac.cn/jssgk/zzjg/kyxt/clqxpzdsys/js/

免试研究生招生信息：http://www.ict.ac.cn/yjsjy/zsxx/sszs/202409/t20240902_7331937.html

欢迎计算机、数学专业的同学申请。有意申请者可以通过以下邮件联系宋老师：songlh.recruiting@gmail.com

You May Also Enjoy

A curated list of awesome Rust checkers

5 minute read

Published:

Migrated to https://github.com/BurtonQin/Awesome-Rust-Checker. Welcome to contribute there.

Table of contents

Linters

NameDescriptionWorking onBug typesTechnologyMaintenance
clippyA bunch of lints to catch common mistakes and improve your Rust code.HIRVersatilePattern matching★★★★★
dylintRun Rust lints from dynamic librariesHIRVersatilePattern matching★★★★★

Static Checkers

NameDescriptionWorking onBug TypesTechnologyMaintenance
MIRAIRust mid-level IR Abstract InterpreterMIRPanic, Security bugs, CorrectnessAbstract Interpretation★★★★★
lockbudStatically detect common memory and concurrrency bugs in Rust. Paper: Safety Issues in Rust, TSE’24MIRDouble-Lock, Conflicting-Lock-Order, Atomicity-Violation, Use-After-Free, Invalid-Free, Panic LocationsData-flow Analysis★★★★★
RAP (formerly SafeDrop)Rust Analysis Platform. Paper: SafeDrop, TOSEM’22MIRUse-After-Free, Double-FreeData-flow Analysis★★★★★
RudraRust Memory Safety & Undefined Behavior Detection. Paper: Rudra, SOSP’21HIR, MIRMemory safety when panicked, Higher Order Invariant, Send Sync VarianceData-flow Analysis★★★☆☆
YugaAutomatically Detecting Lifetime Annotation Bugs in the Rust Language. Paper: Yuga, ICSE’24HIR, MIRLifetime Annotation BugsData-flow Analysis★★★★☆
MirCheckerA Simple Static Analysis Tool for Rust. Paper: MirChecker, CCS’21MIRPanic (including numerical), Lifetime Corruption (memory issues)Abstract Interpretation★★☆☆☆
FFICheckerA Static Analysis Tool For Detecting Memory Management Bugs Between Rust and C/C++. Paper: FFIChecker, ESORICS’22LLVM IRMemory issues across the Rust/C FFIAbstract Interpretation★☆☆☆☆

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
RupairRupair: Towards Automatic Buffer Overflow Detection and Rectification for Rust. Rupair, ACSAC’21AST, MIRBuffer OverflowData-flow Analysis
RCanaryrCanary: Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust. RCanaryHIR, MIRMemory LeaksStatic Program Analysis, Model Checking
CRUSTCRUST: Towards a Unified Cross-Language Program Analysis Framework for Rust. CRUST, QRS’22CRustIR based on MIRSecurity (CFI vilation, Meta Data Leaking, Format String Attack), Memory issues(Out-of-bounds, Use-after-Free, Double-Free, Stack-Overflow, Buffer-Overflow), Arithmetic (Divide-by-zero, Integer-Overflow)Program Analysis Framework
ACORNACORN: Towards a Holistic Cross-Language Program Analysis for Rust. ACORNWasmSecurity (Tainted Variable, Dangerous Function, Format String Attack), Memory issues (Out-of-bounds, Use-after-Free, Double-Free, Stack-Overflow, Buffer-Overflow), Arithmetic (Divide-by-zero, Integer-Overflow)Program Analysis Framework
Yu ZhangStatic Deadlock Detection for Rust Programs. Yu ZhangMIRDeadlockData-flow Analysis
Kaiwen ZhangAutomatically Transform Rust Source to Petri Nets for Checking Deadlocks. Kaiwen ZhangMIRDeadlockPetri Nets

Dynamic Checkers

NameDescriptionWorking onBug TypesTechnologyMaintenance
miriAn interpreter for Rust’s mid-level intermediate representationMIRUndefined BehaviorAbstract Interpretation★★★★★
cargo-carefulExecute Rust code carefully, with extra checking along the way-Undefined BehaviorEnable Debug Assertion in std★★★★★
cargo-fuzzCommand line helpers for fuzzing--Fuzzing★★★★★
LoomConcurrency permutation testing tool for Rust.Source CodeConcurrency BugsPermutation testing★★★★★
ERASANEfficient Rust Address Sanitizer. Paper: IEEES&P’24-Memory Access BugsFuzzing★★★★★
Automated-FuzzerSimple tool to create broken files and checking them with special apps-PanicFuzzing★★★★★
RULFFuzz Target Generator for Rust libraries. Paper: RULF, ASE’21-Out-of-bound, Panic (including arithmetic)Fuzzing★★★☆☆
RPG1RPG: Rust Library Fuzzing with Pool-based Fuzz Target. Paper: RPG, ICSE’24-Out-of-bound, Panic (including arithmetic)Fuzzing★★☆☆☆
SyRustAutomatic Testing of Rust Libraries with Semantic-Aware Program Synthesis. Paper: SyRust, PLDI’21--Program Synthesis★☆☆☆☆
NADERAutomatic Context-Aware Safety Enhancement for Rust. Paper: OOPSLA’21MIR, Source CodeUnchecked IndexingAPI Replacing★☆☆☆☆
casr2collect crash (or UndefinedBehaviorSanitizer error) reports, triage, and estimate severity. Paper: Casr-Cluster, ISPRAS’21, Ivannikov Memorial Workshop’24Crash Reports from ASan, UBSan, GDB-Analyze crashes★★★★★

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
CrabSandwichCrabSandwich: Fuzzing Rust with Rust. CrabSandwich, Fuzzing’23LLVM IROut-of-bounds, PanicFuzzing
Zhiyong RenDetect Stack Overflow Bugs in Rust via Improved Fuzzing Technique. Zhiyong Ren, SEKE’21AST, HIR, MIR, LLVM IRStack OverflowFuzzing
RustheckSafety Enhancement of Unsafe Rust via Dynamic Program Analysis. Rustcheck, QRS-C’23MIRMemory vulnerabilitiesStatic Program Analysis, Instrumentation
  1. The link may be incorrect. See here.
  2. casr analyze the results of dynamic checkers instead of performing dynamic analysis itself. Thanks zjp-CN for recommending casr.

Verifiers1

NameDescriptionWorking onBug TypesTechnologyMaintenance
kaniThe Kani Rust Verifier is a bit-precise model checker for Rust. Paper: kani, ICSE-SEIP’22MIRMemory safety, User-specified assertions, Panics, Unexpected behavior (e.g., arithmetic overflows)Model Checking★★★★★
prustiA static verifier for Rust, based on the Viper verification infrastructure. Paper: prusti, NFM’22 ViperPanic (inluding arithmetic), User-specified assertionsSymbolic Execution★★★★☆
crux-mirA static simulator for Rust programs--Symbolic Testing★★★★☆
verusVerified Rust for low-level systems code. Paper: verus, OOPSLA’23---★★★★★
fluxflux is a refinement type checker for Rust. Paper: flux, PLDI’23---★★★★★
AeneasA verification toolchain for Rust programs. Paper: Aeneas, ICFP’22LLBC (for safe Rust only)--★★★★★
RustBeltFormal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Paper: RustBelt, POPL’18𝜆Rust--★★★★★
RustHornA CHC-based automated verifier for Rust RustHorn, TOPLAS’21MIR--★★★★☆
CreusotA deductive verifier for Rust code. Creusot, ICFEM’22WhyMLPanics, overflows, Assertion failures-★★★★★
RustHornBeltA Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: RustHornBelt, PLDI’22𝜆Rust--★★☆☆☆
RefinedRustA Type System for High-Assurance Verification of Rust Programs. Paper: RefinedRust, PLDI’24Radium--★★★★★

Academic Papers (source code not found yet)

NameDescriptionWorking onBug TypesTechnology
GillianRustA hybrid approach to semi-automated Rust verification. GillianRust---
  1. Thanks to jedbrown for recommending RefinedRust and other Rust-related verification tools.

Thanks to the following awesome works:

  1. https://github.com/analysis-tools-dev/static-analysis?tab=readme-ov-file#rust
  2. https://github.com/analysis-tools-dev/dynamic-analysis?tab=readme-ov-file#rust
  3. A Survey of Rust Language Security Research
  4. RefinedRust: A Type System for High-Assurance Verification of Rust Programs