Content deleted Content added
→Tools: | Add: journal, title. | Use this tool. Report bugs. | #UCB_Gadget |
Citation bot (talk | contribs) Added url. | Use this bot. Report bugs. | Suggested by Headbomb | Linked from Wikipedia:WikiProject_Academic_Journals/Journals_cited_by_Wikipedia/Sandbox | #UCB_webform_linked 773/892 |
||
Line 63:
'''Modeling the environment.''' In this case, the engine instruments the system calls with a model that simulates their effects and that keeps all the side effects in per-state storage. The advantage is that one would get correct results when symbolically executing programs that interact with the environment. The disadvantage is that one needs to implement and maintain many potentially complex models of system calls. Tools such as KLEE,<ref>{{Cite journal|title = KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs|url = http://dl.acm.org/citation.cfm?id=1855741.1855756|journal = Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation|date = 2008-01-01|pages = 209–224|series = OSDI'08|first1 = Cristian|last1 = Cadar|first2 = Daniel|last2 = Dunbar|first3 = Dawson|last3 = Engler}}</ref> Cloud9, and Otter<ref>{{cite web|title=MultiOtter: Multiprocess Symbolic Execution|url=https://www.cs.umd.edu/~mwh/papers/multiotter.pdf|first1 = Jonathan|last1 = Turpie|first2 = Elnatan|last2 = Reisner|first3 = Jeffrey|last3 = Foster|first4 = Michael |last4 = Hicks}}</ref> take this approach by implementing models for file system operations, sockets, [[Inter-process communication|IPC]], etc.
'''Forking the entire system state.''' Symbolic execution tools based on virtual machines solve the environment problem by forking the entire VM state. For example, in S2E<ref>{{Cite journal|title = The S2E Platform: Design, Implementation, and Applications|journal = ACM Trans. Comput. Syst.|date = 2012-02-01|issn = 0734-2071|pages = 2:1–2:49|volume = 30|issue = 1|doi = 10.1145/2110356.2110358|first1 = Vitaly|last1 = Chipounov|first2 = Volodymyr|last2 = Kuznetsov|first3 = George|last3 = Candea|s2cid = 16905399| url=http://infoscience.epfl.ch/record/175469 }}</ref> each state is an independent VM snapshot that can be executed separately. This approach alleviates the need for writing and maintaining complex models and allows virtually any program binary to be executed symbolically. However, it has higher memory usage overheads (VM snapshots may be large).
==Tools==
| |||