Taming Win32 Threads with Static Analysis Slides (08161 yangjasonyue slides)

2020-02-27 58浏览

  • 1.Taming Win32 Threads with Static Analysis Jason Yang Program Analysis Group Center for Software Excellence (CSE) Microsoft Corporation
  • 2.CSE Program Analysis Group • Technologies – PREfix, SAL, ESP, EspX, EspC, … • Defect detection tools – Buffer overrun, Null deref, SQL injection, programmable specification checker, concurrency, …http://www.microsoft.com/windows/cse/pa_home.mspx
  • 3.The Esp Analysis Platform Clients/Specs Concurrency Security Typestate Analysis Analysis Engine and Libraries (Path Refutation, Alias Analysis …) IR CFG; Error Reporting and Suppression; Pattern Matching (OPAL) Front End C/C++/SAL MSIL TSQL JavaScript
  • 4.Locking Problems • • • • • • • Insufficient lock protection Lock order violation Forgetting to release Ownership violation No-suspend guarantee violation UI thread blocking due to SendMessage And more …
  • 5.Win32Multithreading:Plenty of Challenges • Rich set of lock primitives – Critical Section, Mutex, Event, Semaphore, … • “Free-style” acquire/release – Not syntactically scoped • Implicit blocking semantics – SendMessage, LoaderLock, … • How to ensure the intended locking discipline? – Who guards what, who needs to acquire, lock order, …
  • 6.CentralIssue:Locking Disciplines • Essential for avoiding threading errors • Surprisingly hard to enforce in practice – “We have a set of locking conventions to follow” – “They are informally documented” – “We don’t have a way to check against the violations”
  • 7.Checking Concurrency Properties via Sequential Analysis •Insight:Developers mostly reason about concurrent code “sequentially” following locking disciplines •Approach:Mimic developer’s reasoning – Track locking behavior via sequential analysis – Simulate interleaving effects afterwards
  • 8.EspC Concurrency Toolset • • • • Global lock analysis – Global EspC Concurrency annotation – Concurrency SAL Local lock analysis – EspC Lock annotation inference – CSALInfer
  • 9.Global EspC • Global lock analyzer – Deadlock detection – Code mining • Based on ESP – – – – Inter-procedural analysis with function summaries Path-sensitive, context-sensitive Selective merge on dataflow facts Symbolic simulation for path feasibility • “Understands” Win32 threading semantics – Use OPAL specification to capture Win32 locking APIs
  • 10.Phase 1: Lock Sequence Computation Lock(a) {a} Lock(b) {a,b} {a,b} Lock(c) Unlock(a) {b} {a,b,c} Unlock(b) 10 {a,c} {} • Start from root functions • Track lock sequences at each program point • Do not merge if lock sequences are different • Identify locks syntactically based on their types
  • 11.Phase 2: Defect Detection • Deadlock detection – Cyclic locking  deadlock! • Race detection – Insufficient locking  race condition! • Lock misuse patterns – E.g., exit while holding a lock  orphaned lock!
  • 12.Concurrency SAL • Extension to SAL – Covers concurrency properties • Example lock annotations – Lock/data protectionrelation:__guarded_by(cs) int balance; – Caller/callee lockingresponsibility:__requires_lock_held(cs) void Deposit (int amount); – Locking sideeffect:__acquires_lock(cs) void Enter();__releases_lock(cs) void Leave(); – Lock acquisitionorder:__lock_level_order(TunnelLockLevel, ChannelLockLevel); – Threadingcontext:__no_competing_thread void Init();
  • 13.CSALInfer • Concurrency SAL inference engine • Statistics-based inference for in-scope locks – Tracks lock statistics for accessing shared variables – Computes “dominant lock” for shared variable • Constraint-based inference for out-of-scope locks – Generates constraints based on locking events – Translates constraints to propositional formula – Solves constraints via SAT solving • Heuristics-based inference – Looks for strong evidence along a path
  • 14.EspC • Local static lock analyzer – Understands lock annotations – Check violations of Concurrency SAL • Runs on developer’s desktop – PREfast plugin
  • 15.Subset of EspC Warnings • 26100:EspC:'>EspC: