Кіріспе

Бағдарламаны талдау техникасы
Компьютерлік ғылымда символды орындау (сондай-ақ символды бағалау немесе симбекс) – бағдарламаның әр бөлігінің орындалуына қандай кірістер себеп болатынын анықтау үшін бағдарламаны талдау әдісі. Интерпретатор бағдарламаны қадағалайды, қалыпты орындалу кезінде нақты кірістерді алудың орнына кірістер үшін символдық мәндерді қабылдайды. Осылайша ол бағдарламадағы өрнектер мен айнымалылар үшін осы символдар арқылы өрнектерге және әрбір шартты тармақтың мүмкін нәтижелері үшін осы символдар арқылы шектеулерге жетеді. Соңында, тармақты іске қосатын мүмкін кірістерді шектеулерді шешу арқылы анықтауға болады. Символдық модельдеу саласы осы ұғымды аппараттық құралдарға қолданады. Символдық есептеу математикалық өрнектерді талдау үшін осы ұғымды пайдаланады.

Жол жарылысы

Барлық мүмкін бағдарламалық жолдарды символдық түрде орындау үлкен бағдарламалар үшін тиімді емес. Бағдарламадағы мүмкін жолдардың саны бағдарламаның мөлшері артаған сайын экспоненциалды түрде өседі және шексіз циклдар бар бағдарламаларда тіпті шексіз болуы мүмкін. Жолдардың шарықталу мәселесін шешу үшін әдетте жолдарды табуға арналған эвристикалар қолданылады, бұл кодты қамтуды арттырады, тәуелсіз жолдарды параллельдеу арқылы орындау уақытын қысқартады немесе ұқсас жолдарды біріктіреді. Біріктірудің бір мысалы – вертестинг, ол "динамикалық символдық орындаудың әсерін арттыру үшін статикалық символдық орындауды пайдаланады".

Бағдарламаға тәуелді тиімділік

Символды орындау бағдарлама жолын жол бойынша талдау үшін қолданылады, бұл басқа тестілеу әдістері қолданатын (мысалы, динамикалық бағдарлама талдауы) бағдарлама кірісін кіріс бойынша талдаудан артықшылық береді. Дегенмен, егер аздаған кірістер бағдарламада бірдей жолмен өтетін болса, әрбір кірісті жеке-жеке тексеруден көп үнемдеуге болмайды.

Жадының атауын өзгерту

Символдық орындау бірдей жад орны әр түрлі атаулармен қолжетімді болғанда қиындатылады (алиасинг). Алиасингті әрқашан статикалық түрде анықтау мүмкін емес, сондықтан символды орындау механизмі бір айнымалының мәні өзгерсе, екіншісінің де өзгеретінін анықтай алмайды.

Массивтер

Массив көптеген ерекше мәндердің жиынтығы болғандықтан, символдық орындаушылардың бүкіл массивті бір мән ретінде қарастыруы немесе әрбір массив элементін жеке орналасқан жер ретінде қарастыруы қажет. Әрбір массив элементін жеке қарастырудың қиындығы "A[i]" сияқты сілтеме тек i-нің нақты мәні белгілі болғанда ғана динамикалық түрде көрсетілуі мүмкін. Cloud9 және Otter файлдық жүйе операциялары, сокеттер, IPC және т.б. үшін модельдерді жүзеге асыру арқылы осы тәсілді қолданады, соның нәтижесінде бүкіл жүйе күйін көшіреді. Виртуалды машиналарға негізделген символдық орындау құралдары, бүкіл виртуалды машина күйін көшіру арқылы орта проблемасын шешеді. Мысалы, S2E-де әрбір күй – жеке орындала алатын тәуелсіз VM суреті болып табылады. Бұл тәсіл күрделі модельдерді жазу және күту қажеттілігін азайтады және кез келген бағдарламалық кодты символдық түрде орындауға мүмкіндік береді. Дегенмен, бұл жадты көп пайдалануға әкеледі (VM суреттері үлкен болуы мүмкін).

Құралдар

Құралдың мақсатты URL-ы Кез келген адам пайдалана ала ма? Ашық бастапқы код / Жүктеуге болады angr libVEX негізінде (x86, x86 64, ARM, AARCH64, MIPS, MIPS64, PPC, PPC64 және Java қолдауы) http://angr.io/ BE PUM x86 https://github.com/NMHai/BE PUM BINSEC x86, ARM, RISC V (32 бит) http://binsec.github.io crucible LLVM, JVM, және т.б. https://github.com/GaloisInc/crucible ExpoSE JavaScript https://github.com/ExpoSEJS/ExpoSE FuzzBALL VineIL / Native http://bitblaze.cs.berkeley.edu/fuzzball.html GenSym LLVM https://github.com/Generative Program Analysis/GenSym Jalangi2 JavaScript https://github.com/Samsung/jalangi2 janala2 Java https://github.com/ksen007/janala2 JaVerT JavaScript https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2019JaVerT.pdf JBSE Java https://github.com/pietrobraione/jbse jCUTE Java https://github.com/osl/jcute KeY Java http://www.keyproject.org/ Kite LLVM http://www.cs.ubc.ca/labs/isd/Projects/Kite/ KLEE LLVM https://klee.github.io/ Kudzu JavaScript http://webblaze.cs.berkeley.edu/2010/kudzu/kudzu.pdf MPro Ethereum Virtual Machine (EVM) / Native https://sites.google.com/view/smartcontractanalysis/home Maat Ghidra P коды / SLEIGH https://maat.re/ Manticore x86 64, ARMv7, Ethereum Virtual Machine (EVM) / Native https://github.com/trailofbits/manticore/ Mayhem Binary http://forallsecure.com Mythril Ethereum Virtual Machine (EVM) / Native https://github.com/ConsenSys/mythril Otter C https://bitbucket.org/khooyp/otter/overview Oyente NG Ethereum Virtual Machine (EVM) / Native http://www.comp.ita.br/labsca/waiaf/papers/RafaelShigemura paper 16.pdf Pathgrind Native 32 бит Valgrind негізінде https://github.com/codelion/pathgrind Pex .NET Framework http://research.microsoft.com/en-us/projects/pex/ pysymemu x86 64 / Native https://github.com/feliam/pysymemu/ Rosette Racket диалектісі https://emina.github.io/rosette/ Rubyx Ruby http://www.cs.umd.edu/~avik/papers/ssarorwa.pdf S2E x86, x86 64, ARM / Пайдаланушы және ядролық режимдегі екілік файлдар http://s2e.systems/ Symbolic PathFinder (SPF) Java Байткоды https://github.com/SymbolicPathFinder SymDroid Dalvik байткоды http://www.cs.umd.edu/~jfoster/papers/symdroid.pdf SymJS JavaScript https://core.ac.uk/download/pdf/24067593.pdf SymCC LLVM https://www.s3.eurecom.fr/tools/symbolicexecution/symcc.html Triton x86, x86 64, ARM және AArch64 https://triton.quarkslab.com Verifast C, Java https://people.cs.kuleuven.be/~bart.jacobs/verifast

Құралдардың бұрынғы нұсқалары

EXE — KLEE-нің бұрынғы нұсқасы. EXE туралы мақаланы осы жерден табуға болады.