Abstract
Wholly! is an automated build system for the modern software stack. It is designed for reproducible and verifiable builds of optimized and debloated software that runs uniformly on traditional desktops, the cloud, and IoT devices. Wholly! uses Linux containers to ensure the integrity and reproducibility of the build environment. It uses the clang compiler to generate LLVM bitcode for all produced libraries and binaries to allow for whole program analysis, specialization, and optimization. The clang compiler and install tools are all built with Wholly! as well. Wholly! has been applied to build Alpine Linux, Docker containers, microservices, and IoT software. We show that software packages built in Wholly! are faster, smaller, and more amenable to whole program analysis.
L. Gelle—While visiting SRI.
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
References
Alpine Linux. https://alpinelinux.org/
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symposium on Principles of Programming Languages (POPL) (1977)
Docker. https://www.docker.com/
Docker Hub. https://hub.docker.com/
Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10
Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_20
Haskell Lightweight Virtual Machine. https://galois.com/project/halvm/
LinuxKit. https://github.com/linuxkit/linuxkit
Madhavapeddy, A. et al.: Unikernels: library operating systems for the cloud. In: 18th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013)
Malecha, G., Gehani, A., Shankar, N.: Automated software winnowing. In: 30th ACM Symposium on Applied Computing (SAC) (2015)
musl libc. https://www.musl-libc.org/
LLVM musl libc. https://github.com/SRI-CSL/musllvm
OSv. http://osv.io/
Piccolo, S., Frampton, M.: Tools and techniques for computational reproducibility. GigaScience 5(1), 30 (2016)
Rumprun unikernel. https://github.com/rumpkernel/
Smowton, C.: I/O Optimisation and elimination via partial evaluation, Ph.D. thesis, Cambridge University (2014)
Standard Library. https://stdlib.com/
Tuscan Catalog. https://karkhaz.github.io/tuscan/
Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: 32nd ACM Conference on Programming Language Design and Implementation (PLDI) (2011)
Acknowledgement
This material is based upon work supported by the US National Science Foundation (NSF) under Grant ACI-1440800, Department of Homeland Security (DHS) Science and Technology Directorate, and the Office of Naval Research (ONR) under Contract No. N68335-17-C-0558. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of NSF, DHS, or ONR.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Gelle, L., Saidi, H., Gehani, A. (2018). Wholly!: A Build System For The Modern Software Stack. In: Howar, F., Barnat, J. (eds) Formal Methods for Industrial Critical Systems. FMICS 2018. Lecture Notes in Computer Science(), vol 11119. Springer, Cham. https://doi.org/10.1007/978-3-030-00244-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-030-00244-2_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00243-5
Online ISBN: 978-3-030-00244-2
eBook Packages: Computer ScienceComputer Science (R0)