تست امنیت

اجرای نمادین؛ از Path Constraint تا Replay

انتشار در تاریخ توسط محمد عسکری

یک موتور اجرای نمادین گزارش می‌دهد «هدف حساس قابل‌دستیابی است»، حل‌گر یک ورودی تولید می‌کند و داشبورد پوشش شاخه را ۱۰۰٪ نشان می‌دهد. آیا آسیب‌پذیری اثبات شده است؟ هنوز نه. شاید کد تحلیل‌شده با باینری انتشار فرق داشته باشد، فراخوانی بیرونی خلاصه‌سازی شده باشد، عدد صحیح مدل دیگری داشته باشد، ورودی روی اجرای واقعی بازتولید نشود یا اصلاً Oracle فقط یک فرض ضعیف باشد. این راهنما اجرای نمادین (Symbolic Execution) را از یک خروجی جذاب به یک Symbolic Exploration Record قابل‌ممیزی تبدیل می‌کند: Subject، Semantics، Symbolic Input، Path Constraint، Solver Query، Search Budget، Concretization، Test Generation، Concrete Replay، Triage و Evidence.

خلاصه اجرایی: اجرای نمادین چه چیزی می‌گوید؟

  • نتیجه درباره یک Artifact، مدل اجرایی، دامنه ورودی، محیط، فرض‌ها، ابزار و بودجه مشخص است؛ نه «کل نرم‌افزار».
  • SAT یعنی فرمول ارسال‌شده به حل‌گر مدلی دارد؛ به‌تنهایی یعنی باگ، Exploit یا رفتار واقعی نیست.
  • UNSAT نیز فقط در همان فرمول، Theory، مدل و فرض‌ها معنا دارد؛ نبود نقص را ثابت نمی‌کند.
  • مسیر تولیدشده باید با Artifact بومی و همان ورودی Concrete بازاجرا و با Oracle مستقل بررسی شود.
  • پوشش داخلی موتور، پوشش خارجی باینری و پوشش ریسک سه سنجه متفاوت‌اند.
  • پایان کار باید با دلیل توقف، مسیرهای ناتمام، Queryهای Unknown و Concretizationهای رخ‌داده منتشر شود.

اجرای نمادین چیست؟

در اجرای Concrete، متغیر x مقدار معینی مانند ۷ دارد. در اجرای نمادین، x یک عبارت نمادین است و موتور هنگام عبور از شاخه‌ها قیدهای لازم را جمع می‌کند. برای شرط if (x > 10)، یک State قید x > 10 و State دیگر x <= 10 می‌گیرد. حل‌گر SAT/SMT می‌تواند برای یک Path Condition قابل‌ارضاکردن، نمونه‌ای Concrete بسازد. اما موتور یک مدل از اجرا را کاوش می‌کند؛ کیفیت نتیجه به وفاداری همان مدل وابسته است.

چهار خانواده نزدیک اما متفاوت

رویکردحرکت اصلیخروجی معمولمرز مهم
Symbolic Executionاجرای Stateهای نمادینPath، Constraint، Inputمدل و انفجار مسیر
Concolic / Dynamic Symbolicاجرای Concrete همراه قیود نمادینورودی بعدی برای شاخه تازهمسیرهای دیده‌شده و Concretization
Model Checkingکاوش Stateهای یک مدلCounterexample یا نتیجه محدودمدل با برنامه یکی نیست
Fuzzingجهش/تولید ورودی و اجرای واقعیCrash، Coverage، CorpusOracle و رسیدن به قیود دشوار

مرز این راهنما با صفحات دیگر سایت

این صفحه مالک زنجیره Symbolic Exploration Record است. برای عملیات تحلیل استاتیک کد، راهنمای اختصاصی ۹۰۶؛ برای Harness، Corpus و Crash Triage، راهنمای Fuzz Testing؛ برای مدیریت سبد ابزار و Finding، صفحه عملیاتی‌سازی AppSec؛ و برای Property، Proof Obligation و Assurance، راهنمای روش‌های صوری مرجع اصلی‌اند. اجرای نمادین این حوزه‌ها را تکمیل می‌کند، جایگزینشان نیست.

چرا یک Symbolic Exploration Record لازم است؟

عبارت «KLEE پاس شد» بدون نسخه کد، Bitcode، Compiler flags، ورودی نمادین، Search strategy، محدودیت‌ها، Solver و دلیل توقف بازتولیدپذیر نیست. رکورد کاوش باید ادعا را به Subject و Run مقید کند و امکان دهد بازبین بفهمد چه چیزی واقعاً دیده، خلاصه، Concrete، هرس یا اصلاً اجرا نشده است.

ExplorationRecord {
  record_id, claim_id, subject_id, run_id,
  semantics_id, environment_id, assumption_ids[],
  symbolic_inputs[], targets[], search_budget,
  path_summary, solver_summary, concretizations[],
  generated_tests[], native_replays[], findings[],
  termination, limitations[], evidence_ids[], decision
}

ادعا را پیش از اجرا محدود کنید

ادعای خوب می‌گوید: «در Commit و Build مشخص، با مدل عدد صحیح Bit-vector ۳۲-bit، ورودی نمادین چهار‌بایتی، Stub معین برای سرویس بیرونی و بودجه ده‌دقیقه‌ای، موتور یک ورودی برای رسیدن به Predicate مشخص جست‌وجو می‌کند؛ نتیجه درباره Production، Exploitability یا نبود سایر خطاها نیست.» Claim باید Audience، Decision use، Strength، Scope و Not-claimed داشته باشد.

Subject را با Digest تثبیت کنید

Repo URL کافی نیست. Commit، Tree digest، Source/IR/Binary digest، Build ID، Compiler و Flags، Target triple، Optimization level، Dependency lock و Entry point را ثبت کنید. اگر تحلیل روی LLVM IR انجام شده اما Replay روی باینری دیگری است، رابطه Source→IR→Binary باید روشن باشد؛ در غیر این صورت نتیجه میان دو Artifact جابه‌جا شده است.

Semantics بخشی از نتیجه است

موتور باید معنای عملیات را انتخاب کند: پهنای Integer، Signedness، Overflow، Floating point، Pointer و Alignment، Memory model، Undefined behavior، Exception، Thread، Endianness و Encoding. تفاوت Mathematical integer با Bit-vector می‌تواند SAT را به UNSAT یا برعکس تبدیل کند. بهینه‌سازی Compiler نیز شاخه و رفتار Undefined را تغییر می‌دهد.

ورودی نمادین را دقیق تعریف کنید

«Request نمادین» مبهم است. نام، Type، Width، تعداد Byte، Encoding، Grammar، Min/Max، Allowed characters، Length، Nullability، Correlation میان فیلدها و مقادیر حذف‌شده را بنویسید. هر assume فضای کاوش را کوچک می‌کند؛ پس دلیل، مالک، شاهد و اثر آن بر Claim باید قابل‌دیدن باشد.

SymbolicInput {
  id: "SIN-FAKE-01",
  fields: ["amount:int32", "retry:uint8", "status:uint8"],
  constraints: ["0 <= amount <= 500000", "retry <= 2", "status <= 3"],
  encoding: "binary fixture; no HTTP parser",
  excluded: ["database", "network", "real account", "credential"]
}

Domain و Assumption را پنهان نکنید

Domain ممکن است تنها طول ۰ تا ۸، دو Retry و سه Status باشد. Assumption ممکن است Allocator هرگز Fail نشود، Clock ثابت باشد یا Library summary درست عمل کند. این‌ها تنظیمات فرعی نیستند؛ مرز شواهدند. هر فرض باید ASSUMED / MONITORED / TESTED / DISCHARGED / VIOLATED / EXPIRED و اثر نقض داشته باشد.

Symbolic State چیست؟

State معمولاً Program counter، Call stack، حافظه نمادین، Registerها، Constraintها و وضعیت محیط را نگه می‌دارد. شناسه Parent، عمق، تعداد Fork، Digest حافظه و Path Condition اجازه می‌دهد دو State ظاهراً مشابه اشتباه ادغام نشوند. Snapshot کامل می‌تواند بسیار بزرگ باشد؛ Digest و Artifact addressable راه عملی‌تری است.

Path Condition چگونه ساخته می‌شود؟

Path Condition هم‌نهشتی قیودی است که برای رسیدن به یک نقطه لازم بوده‌اند. Source location هر Branch، جهت True/False، عبارت قبل و بعد از Simplification و Mapping آن به IR را ثبت کنید. یک قید ساده‌شده ممکن است منشأ انسانی خود را از دست بدهد؛ بدون Branch trace، Triage سخت می‌شود.

Path P-17:
  B1@checkout.c:41 = true  => amount > 0
  B2@checkout.c:52 = false => retry <= 2
  B3@checkout.c:66 = true  => status == ACCEPTED
  PC = (amount > 0) AND (retry <= 2) AND (status == 2)

Solver Query را یک Artifact بدانید

فرمول، Theoryها، Solver/Version/Digest، Seed، Timeout، Resource limit، Tactic، Cache hit/miss، زمان و Warning را نگه دارید. مستندات رسمی Solver Chain در KLEE حتی هشدار می‌دهد رضایت یک مدل در زبان قید Z3 الزاماً به معنای رضایت همان مدل پس از جای‌گذاری در Expression language خود KLEE نیست؛ بنابراین Validation مدل ارزش عملی دارد.

SAT، UNSAT و UNKNOWN دقیقاً چه می‌گویند؟

  • SAT: Query صورت‌بندی‌شده یک Model دارد؛ ورودی باید Materialize و Replay شود.
  • UNSAT: در Theory، Formula و Assumptionهای ثبت‌شده Model یافت نمی‌شود؛ درباره مدل ناقص یا Production حکم ندهید.
  • UNKNOWN: حل‌گر حکم قطعی نداده؛ Reason unknown و محدودیت را ثبت کنید.
  • TIMEOUT / RESOURCE_LIMIT: نتیجه منفی نیست؛ کار ناتمام است.
  • ERROR / UNSUPPORTED: مسیر به‌خاطر Tool/Model متوقف شده، نه اینکه امن باشد.

Concretization یک رویداد ممیزی است

وقتی موتور برای فراخوانی بیرونی یا عبارت پشتیبانی‌نشده یک مقدار انتخاب می‌کند، فضای جایگزین ممکن است حذف شود. Expression، علت، Policy، مقدار انتخابی، Alternativeها، Stateهای متاثر و Warning را ثبت کنید. سیاست External calls در گزینه‌های رسمی KLEE می‌تواند فراخوانی را ممنوع، فقط با آرگومان Concrete مجاز، یا با Concrete کردن آرگومان نمادین اجرا کند؛ این انتخاب مستقیماً مرز Claim را تغییر می‌دهد.

Fork، Prune و Merge را قابل‌مشاهده کنید

در Branch، State ممکن است Fork شود؛ مسیر Infeasible هرس می‌شود؛ مسیرهای مشابه شاید Merge شوند. شمارش Fork به‌تنهایی کافی نیست. دلیل Prune، Query مربوط، Merge predicate، Stateهای مبدا و اثر Merge بر Solver cost و دقت باید در Summary بیاید.

حلقه و بازگشت چرا خطر انفجار دارند؟

تعداد مسیرها فقط تابع تعداد if نیست. Loop با Bound نمادین، Recursion، Callback، Error handling و Interleaving می‌تواند Stateها را جهشی زیاد کند. Unroll bound، Max depth و State limit باید بخشی از نتیجه باشد. مسیری که پس از پنج دور حلقه قطع شده، درباره دور ششم چیزی نگفته است.

Path Explosion را با عدد گزارش کنید

عبارت «با انفجار مسیر مواجه شدیم» کافی نیست. Stateهای ساخته/فعال/تکمیل/حذف‌شده، Peak memory، Query count و time، مسیرهای Partial، عمق، پوشش و دقیق‌ترین دلیل توقف را منتشر کنید. Denominator ناشناخته را به درصد کامل تبدیل نکنید.

Search Strategy نتیجه را شکل می‌دهد

DFS، Random state، Random path و Coverage-oriented heuristic مسیرهای متفاوتی را در یک بودجه محدود می‌بینند. KLEE در مستندات رسمی چند Search heuristic و Interleaving آن‌ها را توضیح می‌دهد. Strategy، Seed، ترتیب Interleave و Batch size را Pin کنید؛ دو Run با Budget یکسان لزوماً Evidence یکسان ندارند.

بودجه جست‌وجو باید پیشاپیش تعریف شود

Max wall time، CPU، Memory، States، Forks، Depth، Solver time/query، Total query time، Generated tests و Disk را پیش از Run تعیین کنید. تغییر بودجه بعد از دیدن نتیجه می‌تواند Cherry-picking ایجاد کند؛ نسخه جدید Budget را با علت و Correction ثبت کنید.

Environment model را فهرست کنید

Filesystem، Network، Database، Clock، Randomness، OS، Syscall، Library، Allocator و Device یا Concrete، نمادین، Stub، Summary، Passthrough یا Unsupported هستند. «POSIX runtime» به معنای جهان واقعی نیست. هر Stub باید ورودی/خروجی، State، Failure mode و محدودیت داشته باشد.

Library Summary می‌تواند هم نجات‌دهنده و هم منبع خطا باشد

اجرای درون Crypto، Parser یا Database pathها را منفجر می‌کند؛ Summary سرعت می‌دهد. اما Summary ضعیف ممکن است رفتار ناممکن بسازد یا رفتار واقعی را حذف کند. Version، Contract، Exception، Side effect و آزمون تطبیق Summary با Library واقعی را نگه دارید.

حافظه، Pointer و Undefined Behavior

Out-of-bounds، Use-after-free و Alignment به مدل Heap و Pointer وابسته‌اند. Undefined behavior در Source ممکن است در Compiler به رفتار غیرمنتظره تبدیل شود. Instrumentation و Sanitizer لازم را آشکار کنید؛ خود مستندات گزینه‌های KLEE می‌گوید کشف Overflow عدد صحیح به Instrumentation مناسب هنگام ساخت Bitcode وابسته است.

Integer، Floating Point و String یکسان نیستند

Bit-vectorها Wrap دارند؛ Integer ریاضی ندارد. Floating point شامل NaN، Infinity، Signed zero و Rounding است. String Theory، Regex، Unicode normalization و Byte encoding هزینه و معنای متفاوت دارند. در سامانه فارسی، «ی/ی»، «ک/ک»، نیم‌فاصله، رقم‌های فارسی/عربی/لاتین و Bidi را به یک String انتزاعی فرو نکاهید مگر Claim همین انتزاع را پذیرفته باشد.

هم‌زمانی را ساده اعلام نکنید

Race Condition فقط با ورودی ساخته نمی‌شود؛ Scheduler، Memory ordering، Atomicity، Lock، Interrupt و I/O completion دخیل‌اند. موتور تک‌ریسمانی با Environment stub نمی‌تواند «Raceها را آسان پیدا می‌کند» ادعا کند. اگر Thread model یا Schedule exploration ندارید، Concurrency خارج Scope است.

Target و Oracle را جدا کنید

Target می‌تواند Reach یک Line، Assertion failure، Sink یا حالت دامنه باشد. Oracle تعیین می‌کند رفتار مشاهده‌شده درست است یا نه. رسیدن به send() اثبات Data exfiltration نیست؛ Crash نیز همیشه Vulnerability نیست. برای طراحی Expected result و Verdict به راهنمای Test Oracle رجوع کنید.

Bug، Finding و Vulnerability سه وضعیت‌اند

Model trace ابتدا یک Candidate است. پس از Native replay و Oracle review ممکن است Defect شود. Vulnerability علاوه بر Defect به Asset، Attacker، Reachability، Preconditions، Control bypass، Exploitability و Impact نیاز دارد. برچسب شدت را قبل از این زنجیره قطعی نکنید.

Coverage داخلی و خارجی را مخلوط نکنید

Internal coverage ممکن است روی IR و فقط Stateهای موتور محاسبه شود؛ External coverage با اجرای تست‌های تولیدشده روی Artifact بومی سنجیده می‌شود. Denominator، Exclusion، Tool، Optimization و Source mapping را ثبت کنید. ۱۰۰٪ Branch coverage نیز فقط Branchهای ابزارشده را می‌گوید، نه همه Pathها، Requirementها، Riskها یا رفتار محیط.

Test Generation پایان کار نیست

هر تست تولیدی باید Input byte digest، نمایش انسانی، Target path، Setup، Fixture، Command، Timeout، Cleanup و Expected Oracle داشته باشد. Secret scan اجرا کنید و ورودی Model را مستقیم به محیط واقعی نفرستید. تست‌های معادل را Deduplicate کنید، اما ورودی‌های Boundary متفاوت را صرفاً به‌خاطر پوشش مشابه حذف نکنید.

Concrete Replay حلقه اعتبار است

تست ساخته‌شده را روی Artifact بومی با Digest ثبت‌شده، Runtime کنترل‌شده و Oracle مستقل چند بار اجرا کنید. آموزش رسمی Replay تست‌های KLEE نشان می‌دهد فایل‌های تولیدی را می‌توان با Runtime مخصوص روی برنامه بازاجرا کرد. نتیجه را REPRODUCED / NOT_REPRODUCED / ENVIRONMENT_MISMATCH / ORACLE_INCONCLUSIVE / FLAKY ثبت کنید.

عدم بازتولید را پنهان نکنید

عدم Replay ممکن است از Model gap، UB، Compiler، Stub، Concretization، Nondeterminism یا خطای ابزار باشد. آن را False positive فوری ننامید. Triage باید اختلاف Model trace و Native trace را تا اولین Divergence پیدا و Evidence هر دو را نگه دارد.

Triage گام‌به‌گام

  1. Subject، Digest و Run manifest را تطبیق دهید.
  2. ورودی تولیدی را بدون تغییر Replay و Hash کنید.
  3. Oracle و Target را مستقل بازبینی کنید.
  4. Model trace و Native trace را تا اولین Divergence مقایسه کنید.
  5. External call، Summary، Concretization و UB را بررسی کنید.
  6. با Sanitizer یا Instrumentation مستقل، Signal را تایید کنید.
  7. Candidate را Duplicate، Defect، Vulnerability candidate، Tool issue یا Model gap طبقه‌بندی کنید.
  8. Decision و اقدام بعدی را با Owner و Deadline ثبت کنید.

Deduplication بر پایه علت، نه فقط Stack

چند Path می‌توانند به یک Root cause برسند و یک Path می‌تواند چند پیامد داشته باشد. Fingerprint شامل Subject digest، Location، Predicate، First divergence، Signal و Root-cause candidate بسازید. Stack trace یا Line number به‌تنهایی با Refactor ناپایدار است.

Run Manifest حداقل لازم

RunManifest {
  run_id, subject_digest, ir_digest, container_digest,
  engine_version, solver_version, plugin_versions,
  command_digest, config_digest, search_strategy, seed,
  time_memory_state_query_budgets,
  environment_model, assumptions, targets,
  start_end_utc, termination_reason,
  stdout_stderr_warning_digests, artifact_index
}

Evidence Pack چه چیزهایی دارد؟

Claim، Subject/Build manifest، Symbolic input schema، Assumption register، Environment model، Run manifest، Query log یا Digest، Path summary، Concretization log، Generated tests، Replay records، Coverage reports، Findings، Triage، Decision و Correction chain را با Digest و Retention کنار هم بگذارید. Evidence بدون Provenance فقط یک فایل است.

KLEE را چگونه دقیق توصیف کنیم؟

KLEE یک موتور اجرای نمادین بر LLVM است که می‌تواند ورودی نمادین، Path و تست تولید کند. نسخه، IR، Runtime، Search options، Solver، External-call policy، Warningها و فایل خروجی را ثبت کنید. موفقیت یک Tutorial را به سازگاری همه برنامه‌های C/C++ یا تضمین نبود خطا تعمیم ندهید.

angr برای چه مسئله‌ای مناسب است؟

مستندات رسمی angr اجرای نمادین روی State و Expressionهای Claripy را توضیح می‌دهد. در تحلیل Binary، Loader، Architecture، SimProcedure، Hook، Calling convention و Address target بخشی از Subject/Environment هستند. Summary تابع کتابخانه‌ای می‌تواند Path explosion را کم کند، ولی باید به‌عنوان Model ثبت و اعتبارسنجی شود.

S2E و اجرای نمادین انتخابی

S2E اجرای نمادین انتخابی را با ماشین مجازی و تحلیل System stack ترکیب می‌کند. «اجرای نرم‌افزار تغییرنیافته» به معنای نمادین‌شدن کامل همه محیط نیست؛ Selector، Plugin، Concrete/symbolic transition، Guest image و تحلیل‌گر Property باید در رکورد بیایند.

Concolic Execution چه مصالحه‌ای می‌سازد؟

Concolic یک اجرای Concrete را دنبال و هم‌زمان قیدها را جمع می‌کند؛ سپس یک Branch condition را Negate می‌کند تا ورودی بعدی ساخته شود. این روش با محیط واقعی بهتر تعامل می‌کند، اما تنها مسیر Concrete مشاهده‌شده را نمادین می‌سازد و در نقاط Unsupported ممکن است مقدار را Concrete کند. Seed corpus و انتخاب Branch بعدی بخشی از Search policy است.

اجرای نمادین در برابر Fuzzing

Fuzzing «کور» نیست؛ بسیاری از Fuzzerها Coverage-guided، Grammar-aware یا Constraint-assisted هستند. اجرای نمادین نیز همیشه عمیق‌تر نیست؛ Query دشوار یا مدل ضعیف آن را متوقف می‌کند. ترکیب عملی می‌تواند Corpus فاز را به Seed تبدیل کند و ورودی نمادین تولیدشده را پس از Replay وارد Corpus کند، با حفظ Provenance و جلوگیری از نسبت‌دادن Coverage یک ابزار به دیگری.

اجرای نمادین در برابر Formal Verification

اجرای نمادین می‌تواند بخشی از یک استدلال صوری باشد، اما هر Run محدود Formal proof نیست. Search budget، Unsupported operation و محیط ناقص معمولاً نتیجه را Partial می‌کنند. Proof claim به Property معتبر، Proof obligation، Assumption discharge، Tool/TCB و Refinement نیاز دارد؛ این صفحه فقط Evidence کاوش را مالک است.

اجرای نمادین در برابر Static Analysis

برچسب Static/Dynamic برای همه ابزارها کافی نیست. اجرای نمادین می‌تواند Source/IR/Binary را بدون اجرای بومی تفسیر کند؛ Concolic یک اجرای واقعی دارد. Abstract interpretation معمولاً روی Fixpoint و Over-approximation کار می‌کند، درحالی‌که Symbolic executor State/Path مشخص را دنبال می‌کند. نتیجه ابزار را با Semantics واقعی آن نام‌گذاری کنید.

Mutation به اعتبار Oracle و Harness کمک می‌کند

Mutant می‌تواند نشان دهد Target/Oracle نسبت به یک تغییر حساس است، اما Mutation score اثبات کامل‌بودن کاوش نیست. راهنمای Mutation Testing را برای طراحی اپراتور، Equivalent mutant و Triage جداگانه استفاده کنید. Mutant digest و نسبت آن با Subject اصلی را در Evidence بیاورید.

CI/CD: اجرای کوتاه و Campaign عمیق را جدا کنید

روی Pull Request، Subjectهای تغییرکرده، Budget کوتاه و Targetهای بحرانی را اجرا کنید؛ Campaign زمان‌بر را زمان‌بندی‌شده نگه دارید. Cache باید به Source/IR/Config/Solver digest متصل باشد. Artifact، Log، Test و Summary را منتشر کنید و Gate را فقط روی Resultهای بازتولیدشده و Policy روشن اعمال کنید. برای Pipeline as Code از راهنمای CI/CD تست خودکار استفاده کنید.

واژگان نتیجه را استاندارد کنید

PATH_FEASIBLE_MODEL
PATH_INFEASIBLE_MODEL
QUERY_UNKNOWN
QUERY_TIMEOUT
PATH_PARTIAL
TARGET_REACHED_MODEL
TEST_GENERATED
REPLAY_REPRODUCED
REPLAY_NOT_REPRODUCED
ORACLE_INCONCLUSIVE
FINDING_CONFIRMED
MODEL_GAP
TOOL_ERROR
STALE_EVIDENCE

مرز ادعای امنیت، Safety و انطباق

رسیدن نمادین به Sink یک Threat hypothesis است؛ Exploitability و Impact باید در محیط مجاز و ایمن جداگانه اعتبارسنجی شوند. Safety به Hazard، محیط عملیاتی، Fault، Mitigation و مرجع پذیرش ریسک نیاز دارد. Compliance و حریم خصوصی نیز از یک Path نتیجه نمی‌شوند. هیچ ورودی تولیدی را بدون مجوز به سامانه ثالث یا Production ارسال نکنید.

آزمایشگاه فارسی و کاملاً ساختگی Checkout

این آزمایشگاه آفلاین است و هیچ شبکه، بانک، PSP، حساب، شخص، داده واقعی، Cookie، Token یا Credential ندارد. تابع ساختگی یک amount، retry و status می‌گیرد. هدف Model این است که آیا State خیالی POSTED_TWICE با یک EventID دست‌یافتنی است. مبلغ فقط Fixture آموزشی با واحد IRR است؛ نمایش تومان صرفاً Presentation و غیرحسابداری است.

function fakeCheckout(amount, retry, status) {
  if (amount <= 0 || amount > 500000) return "REJECTED";
  if (status !== 2) return "PENDING";
  let postings = 1;
  if (retry === 2 && amount % 7 === 0) postings++;
  return postings === 2 ? "POSTED_TWICE" : "POSTED_ONCE";
}

Domain: int32 amount in [0,500000], uint8 retry in [0,2], status in [0,3]
Target: return == "POSTED_TWICE"
Not modeled: parser, HTTP, DB, network, clock, concurrency, crash, real ledger

رکورد Candidate آزمایشگاه

RUN=RUN-SYM-FAKE-001
SUBJECT=fixture.js@sha256:fictional
PATH=(amount>0) AND (amount<=500000) AND (status=2) AND (retry=2) AND (amount mod 7=0)
SOLVER_RESULT=SAT
MODEL={amount:7,retry:2,status:2}
TARGET_REACHED_MODEL=true
NATIVE_REPLAY=false
DECISION=CANDIDATE_MODEL_ONLY
BOUNDARY=no production, security, accounting, or real payment claim

سناریوهای فارسی آزمایشگاه

  • مقادیر ۷، ۷+ و ۰۰۰٬۰۰۰٬۷ با رقم فارسی، عربی و لاتین فقط در لایه نمایش؛ Parser اصلاً مدل نشده است.
  • «تایید»، «تأیید»، ی/ی، ک/ک و نیم‌فاصله برای نشان‌دادن شکاف Encoding؛ تابع فقط Status عددی می‌بیند.
  • UTC و Asia/Tehran و تاریخ جلالی صرفاً Metadata نمایش‌اند؛ Clock در Subject وجود ندارد.
  • ورودی دیررس، Duplicate callback، Crash-before/after fake commit و Reorder به‌عنوان سناریوی خارج مدل ثبت می‌شوند، نه نتیجه Run.
  • یک تغییر عمدی در Mapping از status=2 به status=3 برای ایجاد Replay mismatch و آموزش Triage استفاده می‌شود.

Validator قطعی آزمایشگاه چه می‌کند؟

Validator مستقل و بدون Dependency، Schema رکورد را به کنترل‌های Group-qualified تبدیل و یکتایی را بررسی می‌کند. سپس یک Checker سطحی با دیدن «Run کامل، SAT، Input، Target و پوشش ۱۰۰٪» اشتباه می‌گوید ALL_PATHS_COVERED_VULNERABILITY_PROVEN. ممیزی نبود Replay، کامل‌نبودن محیط و مسیرها را آشکار و نتیجه را Hold می‌کند. پس از Pin شدن Subject/Semantics/Domain/Assumption/Budget/Termination/Concretization و ثبت Replay ناموفق، خروجی محدود READY_FOR_SYMBOLIC_EXPLORATION_REVIEW-0 است؛ نه اثبات نقص یا امنیت.

CONTROL_COUNT=335
SUPERFICIAL=ALL_PATHS_COVERED_VULNERABILITY_PROVEN
AUDIT=HOLD-335
INDEPENDENT_TARGET=real-system-or-production:false:PASS
CORRECTED=READY_FOR_SYMBOLIC_EXPLORATION_REVIEW-0
BOUNDARY=model-and-fixture-only; no all-path, bug, vulnerability, exploitability, security, safety, compliance, or production claim

دروازه تصمیم پیشنهادی

اگر Subject یا Semantics Pin نیست، Run قابل‌استناد نیست. اگر Query نتیجه قطعی ندارد، INCONCLUSIVE است. اگر Target فقط در Model رسیده، Candidate است. اگر Native replay و Oracle مستقل تایید شدند، Finding می‌تواند Confirmed شود. برچسب Vulnerability تنها پس از Threat/Exploitability/Impact review مجاز است. هر تغییر Artifact، Environment model، Solver یا Assumption باید Impact analysis و در صورت نیاز Rerun ایجاد کند.

تغییر، انقضا و Correction

Evidence به Commit و Config وابسته است. تغییر Compiler، Dependency، Summary، Solver یا Target می‌تواند آن را Stale کند. رکورد قبلی را پاک نکنید؛ Correction شامل گزاره قدیمی، علت، زمان کشف، گزاره جدید، تصمیم‌های متاثر، Notification و Approver باشد. تاریخچه غیرقابل‌تغییر از داشبورد سبز مهم‌تر است.

۲۰ ضدالگوی رایج

این ضدالگوها را Red flag بدانید: «همه مسیرها» بدون Denominator؛ ۱۰۰٪ Coverage مساوی نبود باگ؛ SAT مساوی Exploit؛ UNSAT مساوی امن؛ نادیده‌گرفتن UNKNOWN؛ Repo بدون Commit؛ Source بدون IR/Binary mapping؛ Solver بدون نسخه؛ Query بدون Timeout؛ Assumption پنهان؛ External call خاموش؛ Concretization بی‌گزارش؛ Stub بدون Contract؛ Loop bound بی‌ذکر؛ Race claim با مدل تک‌ریسمانی؛ Test بدون Replay؛ Replay روی Build دیگر؛ Target بدون Oracle؛ Severity پیش از Impact؛ و حذف Run قدیمی پس از Correction.

چک‌لیست بازبینی مالک

  • Claim، Scope، Strength، Decision use و Not-claimed نوشته شده‌اند.
  • Source/IR/Binary/Build و همه Digestها قابل‌ردیابی‌اند.
  • Integer، Float، Memory، UB، Thread و Encoding model مشخص‌اند.
  • ورودی، Domain، Constraint و همه Assumptionها نسخه‌دارند.
  • Environment و External callها Concrete/Symbolic/Stub/Unsupported برچسب دارند.
  • Engine، Solver، Plugin، Container، Command و Config Pin شده‌اند.
  • Strategy، Seed و تمام Budgetها پیش از Run ثبت شده‌اند.
  • Fork/Prune/Merge/Concretization/Unknown/Timeout قابل‌مشاهده‌اند.
  • Coverage دارای Scope و Denominator و Internal/External label است.
  • Generated input دارای Digest، Fixture، Oracle و Secret scan است.
  • Native replay روی Artifact درست و چندباره انجام شده است.
  • Finding از Candidate، Defect و Vulnerability تفکیک شده است.
  • Evidence Pack، Retention، Access و Provenance کامل‌اند.
  • تغییر و Correction می‌تواند Evidence را Stale کند.
  • هیچ داده، Credential یا سامانه واقعی بدون مجوز وارد Run نشده است.

پایلوت ۳۰روزه بدون سامانه واقعی

هفته اول فقط Fixture ساختگی، Claim و Subject/Semantics/Environment contract؛ هفته دوم Runهای کوتاه با دو Strategy و ثبت Budget/Termination؛ هفته سوم تولید تست، Native replay و First-divergence triage؛ هفته چهارم Evidence Pack، Mutation محدود، CI غیرمسدودکننده و Review مستقل. معیار موفقیت «تعداد باگ» نیست: نرخ Replay، سهم Unknown/Timeout، شکاف مدل کشف‌شده، زمان Triage، پایداری Run و تصمیم‌های قابل‌ردیابی را بسنجید.

جمع‌بندی

اجرای نمادین یک نقشه جادویی از «تمام رفتارهای ممکن» نیست. یک آزمایش محاسباتی روی Artifact و مدل معین است که با قید مسیر و حل‌گر، Stateها را در بودجه محدود کاوش می‌کند. ارزش واقعی وقتی ایجاد می‌شود که Result از Model به ورودی Concrete، Replay مستقل، Oracle، Triage و Evidence پیوند بخورد و هر Limit آشکار بماند.

پرسش‌های متداول

آیا اجرای نمادین همه مسیرهای برنامه را بررسی می‌کند؟

معمولاً خیر. انفجار مسیر، حلقه، محیط، عملیات پشتیبانی‌نشده و بودجه باعث کاوش Partial می‌شوند. حتی Completion در یک Domain محدود به معنای همه رفتارهای Production نیست.

آیا SAT یعنی یک باگ واقعی پیدا شده است؟

نه. SAT فقط مدل‌داشتن Query را می‌گوید. ورودی باید ساخته، روی Artifact بومی بازاجرا و با Oracle مستقل تایید شود؛ سپس اثر و طبقه‌بندی بررسی می‌شوند.

تفاوت اجرای نمادین و Concolic چیست؟

اجرای نمادین Stateهای نمادین را مستقیماً تفسیر می‌کند؛ Concolic یک اجرای Concrete را همراه قیود دنبال می‌کند و با Negate کردن قید، ورودی بعدی می‌سازد. هر دو به مدل، Solver و Search policy وابسته‌اند.

آیا اجرای نمادین جای Fuzzing و تست واحد را می‌گیرد؟

خیر. Fuzzing اجرای واقعی و Corpus/Coverage متفاوتی دارد؛ تست واحد Oracle و قرارداد قابل‌نگهداری می‌سازد. بهترین ترکیب، تبادل ورودی و Evidence با Provenance روشن است.

حداقل خروجی قابل‌ممیزی یک Run چیست؟

Claim، Subject و Digest، Semantics، Input/Domain، Environment/Assumption، نسخه ابزار و Solver، Strategy/Budget، Path/Query/Concretization summary، Termination، Generated tests، Replay، Findings، Limitations و Evidence index.

محمد عسکری

محمد هستم، توسعه‌دهنده وب با بیش از ده سال تجربه در برنامه‌نویسی سمت سرور و کاربر. به یادگیری و اشتراک‌گذاری دانش علاقه‌مندم و اخیراً تمرکزم را روی حوزه تست نرم‌افزار گذاشته‌ام تا تجربیاتم را در این زمینه نیز به اشتراک بگذارم و به درک بهتر کیفیت نرم‌افزار کمک کنم.

دیدگاهتان را بنویسید