Movec is an automated tool for runtime MOnitoring and VErification 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 memory error is detected, an error message is reported automatically. The user may also specify customized runtime behavior for the specified properties, e.g., forcing the program to abort or executing 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 primarily in two aspects. First, it uses a smart-status-based monitoring algorithm (cf. ISSTA'21, TOSEM'24), which is more effective in detecting memory errors than traditional approaches. Second, it uses a source-level instrumentation framework (cf. ISSTA'19, TSE'23), i.e., it directly rewrites the source code written by the programmer instead of the IR or binary code produced by a compiler, which makes Movec insensitive to compiler optimizations and platform-independent.
• Aspect-oriented programming (AOP). Movec automatically weaves aspect (monitor) specifications written in the Aclang language (an aspect-oriented C programming language) into Movec-unaware C programs. The Aclang language can define pointcuts and advices concerning program's internal events such as calling/executing functions and getting/setting variable values (cf. OOPSLA'24).
• Monitoring-oriented programming (MOP). Movec automatically weaves aspect (monitor) specifications (with properties and their handlers being specified) written in the Movec language (an extension of Aclang) 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).

Download

• Movec version 0.9.0 for Ubuntu 64-bit
  This package contains not only Movec, but also examples of using Movec for memory safety and AOP. Furthermore, it contains the SARD benchmark suite and the MSBench benchmark suite below (also called Memsafe in our papers), and the Nptrs benchmark suite.
• The MiBench and SPEC benchmark suites
• Movec-MSBench: A memory safety benchmark suite
• A formal operational semantics of the Smatus approach
• Movec-RVBench: A runtime verification benchmark suite

To run Movec, please put its executable file in a directory in your PATH. Note that:

• Movec is developed and tested under Ubuntu 22.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.
• If you are not familiar with the user instructions and the syntax of Aclang and Movec (for writing aspects and monitors), please learn from the examples and benchmarks.

References and Documentations

• Zhe Chen, Yunlong Zhu, Zhemin Wang. Design and implementation of an aspect-oriented C programming language. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2024), Pasadena, California, United States, October 20–25, 2024, Proceedings of the ACM on Programming Languages (PACMPL), 8(OOPSLA1):??-??, ACM, 2024. [Artifact and Reproduction Package]
• Zhe Chen, Rui Yan, Yingzi Ma, Yulei Sui, Jingling Xue. A smart status based monitoring algorithm for the dynamic analysis of memory safety. ACM Transactions on Software Engineering and Methodology, accepted, ACM, 2024.
• Zhe Chen, Qi Zhang, Jun Wu, Junqi Yan, and Jingling Xue. A source-level instrumentation framework for the dynamic analysis of memory safety. IEEE Transactions on Software Engineering, 49(4):2107-2127, IEEE, 2023.
• Zhe Chen, Jun Wu, Qi Zhang, Jingling Xue. A dynamic analysis tool for memory safety based on smart status and source-level instrumentation. In Proceedings of the 44th ACM/IEEE International Conference on Software Engineering (ICSE 2022), DEMO Track, Pittsburgh, USA, May 22-27, 2022, Companion Volume, pp. 6-10, ACM, 2022.
• 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. [Artifact and Reproduction Package]
• 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)