Abstract
Formal verification of the Linux kernel has been receiving increasing attention in recent years, with the development of many models, from memory subsystems to the synchronization primitives of the real-time kernel. The effort in developing formal verification methods is justified considering the large code-base, the complexity in synchronization required in a monolithic kernel and the support for multiple architectures, along with the usage of Linux on critical systems, from high-frequency trading to self-driven cars. Despite recent developments in the area, none of the proposed approaches are suitable and flexible enough to be applied in an efficient way to a running kernel. Aiming to fill such a gap, this paper proposes a formal verification approach for the Linux kernel, based on automata models. It presents a method to auto-generate verification code from an automaton, which can be integrated into a module and dynamically added into the kernel for efficient on-the-fly verification of the system, using in-kernel tracing features. Finally, a set of experiments demonstrate verification of three models, along with performance analysis of the impact of the verification, in terms of latency and throughput of the system, showing the efficiency of the approach.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
These can be obtained for example by running: sudo cat /sys/kernel/debug/tracing/available_events.
- 2.
The tools, the verification modules, the BUG report, high-resolution figures and FAQ are available in the companion page [32].
- 3.
Note that supporting the full model in [33] is not yet possible with the tool being presented in this paper, due to additional changes needed within the kernel. Therefore, this is still work in progress.
- 4.
This is a restriction from [33].
References
Akesson, K., Fabian, M., Flordal, H., Malik, R.: Supremica - an integrated environment for verification, synthesis and simulation of discrete event systems. In: 2006 8th International Workshop on Discrete Event Systems, pp. 384–385, July 2006. https://doi.org/10.1109/WODES.2006.382401
Alglave, J., Maranget, L., McKenney, P.E., Parri, A., Stern, A.: Frightening small children and disconcerting grown-ups: concurrency in the Linux Kernel. In: Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2018, pp. 405–418. ACM, New York (2018). https://doi.org/10.1145/3173162.3177156
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: Technical Report MSR-TR-2004-08 - SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft - Microsoft Research, January 2004. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2004-08.pdf
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002, pp. 1–3. ACM, New York (2002). https://doi.org/10.1145/503272.503274
Basler, G., Donaldson, A., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: satabs: a bit-precise verifier for C programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 552–555. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_47
Blackham, B., Shi, Y., Chattopadhyay, S., Roychoudhury, A., Heiser, G.: Timing analysis of a protected operating system kernel. In: Proceedings of the 32nd IEEE Real-Time Systems Symposium (RTSS11), Vienna, Austria, pp. 339–348, November 2011
Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2010)
Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng. 30(6), 388–402 (2004). https://doi.org/10.1109/TSE.2004.22
Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Formal Aspects Comput. 17(4), 461–483 (2005). https://doi.org/10.1007/s00165-005-0071-z
Chishiro, H.: RT-Seed: real-time middleware for semi-fixed-priority scheduling. In: 2016 IEEE 19th International Symposium on Real-Time Distributed Computing (ISORC) (2016)
Condliffe, J.: U.S. military drones are going to start running on Linux, July 2014. https://gizmodo.com/u-s-military-drones-are-going-to-start-running-on-linu-1572853572
Corbet, J.: The kernel lock validator, May 2006. https://lwn.net/Articles/185666/
Corbet, J.: Linux at NASDAQ OMX, October 2010. https://lwn.net/Articles/411064/
Corbet, J.: Jump label, October 2010. https://lwn.net/Articles/412072/
Cotroneo, D., Di Leo, D., Natella, R., Pietrantuono, R.: A case study on state-based robustness testing of an operating system for the avionic domain. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 213–227. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24270-0_16
Cotroneo, D., Leo, D.D., Fucci, F., Natella, R.: SABRINE: state-based robustness testing of operating systems. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Piscataway, NJ, USA, pp. 125–135. IEEE Press (2013). https://doi.org/10.1109/ASE.2013.6693073
Cucinotta, T., et al.: A real-time service-oriented architecture for industrial automation. IEEE Trans. Ind. Inform. 5(3), 267–277 (2009). https://doi.org/10.1109/TII.2009.2027013
Dronamraju, S.: Linux kernel documentation - uprobe-tracer: Uprobe-based event tracing, May 2019. https://www.kernel.org/doc/Documentation/trace/uprobetracer.txt
Dubey, A., Karsai, G., Abdelwahed, S.: Compensating for timing jitter in computing systems with general-purpose operating systems. In: 2009 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, pp. 55–62, March 2009. https://doi.org/10.1109/ISORC.2009.28
Ellson, J., Gansner, E., Koutsofios, L., North, S.C., Woodhull, G.: Graphviz—open source graph drawing tools. In: Mutzel, P., Jünger, M., Leipert, S. (eds.) GD 2001. LNCS, vol. 2265, pp. 483–484. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45848-4_57
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2002, pp. 58–70. ACM, New York (2002). https://doi.org/10.1145/503272.503279
Hiramatsu, M.: Linux tracing technologies: Kprobe-based event tracing, May 2019. https://www.kernel.org/doc/html/latest/trace/kprobetrace.html
Klein, G., et al.: seL4: formal verification of an OS Kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207–220. ACM, New York (2009). https://doi.org/10.1145/1629575.1629596
Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_26
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994). https://doi.org/10.1145/177492.177726
Lei, B., Liu, Z., Morisset, C., Li, X.: State based robustness testing for components. Electron. Notes Theoret. Comput. Sci. 260, 173–188 (2010). https://doi.org/10.1016/j.entcs.2009.12.037
Linux Kernel Documentation: Linux tracing technologies, May 2019. https://www.kernel.org/doc/html/latest/trace/index.html
Marinas, C.: Formal methods for kernel hackers (2018). https://linuxplumbersconf.org/event/2/contributions/60/attachments/18/42/FormalMethodsPlumbers2018.pdf
Matni, G., Dagenais, M.: Automata-based approach for kernel trace analysis. In: 2009 Canadian Conference on Electrical and Computer Engineering, pp. 970–973, May 2009. https://doi.org/10.1109/CCECE.2009.5090273
de Oliveira, D.B.: How can we catch problems that can break the preempt\(\_\)rt preemption model? November 2018. https://linuxplumbersconf.org/event/2/contributions/190/
de Oliveira, D.B.: Mind the gap between real-time linux and real-time theory, November 2018. https://www.linuxplumbersconf.org/event/2/contributions/75/
de Oliveira, D.B.: Companion page: Efficient formal verification for the linux kernel, May 2019. http://bristot.me/efficient-formal-verification-for-the-linux-kernel/
de Oliveira, D.B., Cucinotta, T., de Oliveira, R.S.: Untangling the intricacies of thread synchronization in the PREEMPT\(\_\)RT Linux Kernel. In: Proceedings of the IEEE 22nd International Symposium on Real-Time Distributed Computing (ISORC), Valencia, Spain, May 2019
de Oliveira, D.B., de Oliveira, R.S.: Timing analysis of the PREEMPT\(\_\)RT Linux kernel. Softw.: Pract. Exp. 46(6), 789–819 (2016). https://doi.org/10.1002/spe.2333
Phoronix Test Suite: Open-source, automated benchmarking, May 2019. www.phoronix-test-suite.com
Poimboeuf, J.: Introducing kpatch: dynamic kernel patching, February 2014. https://www.redhat.com/en/blog/introducing-kpatch-dynamic-kernel-patching
Pullum, L.L.: Software Fault Tolerance Techniques and Implementation. Artech House Inc., Norwood (2001)
Rostedt, S.: Secrets of the Ftrace function tracer. Linux Weekly News, January 2010. http://lwn.net/Articles/370423/. Accessed 09 May 2017
San Vicente Gutiérrez, C., Usategui San Juan, L., Zamalloa Ugarte, I., Mayoral Vilches, V.: Real-time Linux communications: an evaluation of the Linux communication stack for real-time robotic applications, August 2018. https://arxiv.org/pdf/1808.10821.pdf
Shahpasand, R., Sedaghat, Y., Paydar, S.: Improving the stateful robustness testing of embedded real-time operating systems. In: 2016 6th International Conference on Computer and Knowledge Engineering (ICCKE), pp. 159–164, October 2016. https://doi.org/10.1109/ICCKE.2016.7802133
Spear, A., Levy, M., Desnoyers, M.: Using tracing to solve the multicore system debug problem. Computer 45(12), 60–64 (2012). https://doi.org/10.1109/MC.2012.191
The Linux Foundation: Automotive grade Linux, May 2019. https://www.automotivelinux.org/
Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering, ASE 2007, pp. 501–504. ACM, New York (2007).https://doi.org/10.1145/1321631.1321719
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
de Oliveira, D.B., Cucinotta, T., de Oliveira, R.S. (2019). Efficient Formal Verification for the Linux Kernel. In: Ölveczky, P., Salaün, G. (eds) Software Engineering and Formal Methods. SEFM 2019. Lecture Notes in Computer Science(), vol 11724. Springer, Cham. https://doi.org/10.1007/978-3-030-30446-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-30446-1_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-30445-4
Online ISBN: 978-3-030-30446-1
eBook Packages: Computer ScienceComputer Science (R0)