Movec is an automated tool for runtime MOnitoring, VErification and Control of C programs as an extension to the C programming language. Movec provides a source-to-source transformation that statically analyzes input C programs and generates instrumented C programs which can be compiled by any compliant C compiler such as GCC and other platform-specific compilers. By running the compiled programs, memory safety and the specified properties can be automatically monitored and verified at runtime. When a violation is detected, an error message is reported. The user may also specify other control behavior for the violation, e.g., force the program to abort or execute a code snippet for recovery purposes. Movec can be used with fuzzy testing, like other dynamic analysis tools.
In particular, Movec implements the following three features:
- Dynamic analysis of C memory safety. Movec is different from other dynamic analysis tools in two aspects. First, it uses a smart-status-based monitoring algorithm (cf. ISSTA'21), which is more effective in detecting errors than traditional approaches. Second, it uses a source-level instrumentation framework (cf. ISSTA'19), i.e., rewrites the code written by the programmer instead of the IR or binary code, which makes Movec insensitive to compiler optimizations and platform-independent.
- Aspect-oriented programming (AOP). Movec automatically weaves aspect (monitor) specifications written in the Movec language into Movec-unaware C programs. The Movec language can define pointcuts and actions concerning program's internal events such as calling/executing functions and getting/setting variable values.
- Monitoring-oriented programming (MOP). Movec automatically weaves monitor specifications (with properties and their handlers) written in the Movec language into Movec-unaware C programs. The Movec language can define formal properties written in regular expressions, finite state machines and temporal logics (cf. TACAS'16).
To run Movec, please put its executable file in a directory in your PATH. Note that:
- Movec is developed and tested under Ubuntu 16.04 64-bit. It may also work under other compatible Linux releases, but we cannot guarantee that.
- You can use "movec --version" to show its version, "movec -h" to show user instructions. But note that some of the listed options are not available in this version, and using them takes no effect. The AOP and MOP features were available in an old version, but not in this version. We are refactoring their implementation and they will be included in a future version (will be released soon).
- If you are not familiar with the user instructions and the syntax of monitors, please learn from the examples and benchmarks.
References and Documentations
Zhe Chen, Chong Wang, Junqi Yan, Yulei Sui, Jingling Xue.
Runtime Detection of Memory Errors with Smart Status.
In Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2021), Virtual, Denmark, July 11–17, 2021, pp. 296-308. ACM, 2021.
Zhe Chen, Junqi Yan, Shuanglong Kan, Ju Qian, Jingling Xue.
Detecting Memory Errors at Runtime with Source-Level Instrumentation.
In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2019), July 15-19, 2019, pp. 341-351. ACM, 2019. (ACM SIGSOFT Distinguished Paper Award)
Zhe Chen, Chuanqi Tao, Zhiyi Zhang, Zhibin Yang.
Beyond Spatial and Temporal Memory Safety.
In Proceedings of the ACM/IEEE 40th International Conference on Software Engineering (ICSE 2018), Gothenburg, Sweden, May 27-June 3, 2018, Companion Volume, pp. 189-190. ACM, 2018.
Zhe Chen, Junqi Yan, Wenming Li, Ju Qian, Zhiqiu Huang.
Runtime verification of memory safety via source transformation.
In Proceedings of the ACM/IEEE 40th International Conference on Software Engineering (ICSE 2018), Gothenburg, Sweden, May 27-June 3, 2018, Companion Volume, pp.264-265. ACM, 2018.
Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang.
Parametric Runtime Verification of C Programs.
In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Eindhoven, The Netherlands, April 2-8, 2016, Lecture Notes in Computer Science, vol. 9636, pp. 299-315. Springer, 2016.
The Movec Reference Manual gives a tutorial from a user's point of view and describes how to write monitor specifications and run the tool. (in progress)