BriefCASE Framework
Overview
Formal methods tools that provide mathematical proof of system security properties have improved dramatically in their power and capabilities. Our team has developed BriefCASE, a model-based systems engineering environment that integrates formal methods at all levels of system design. Our methodology and tools enable systems engineers to address cybersecurity concerns early in the development of complex high-assurance systems.
Document
Playlist
-
BriefCASE Demo
-
BriefCASE demo part 2
Links
Framework Tools
Acknowledgements
-
Developed by Collins Aerospace
Contacts
-
Isaac Amundson, Collins Aerospace, isaac dot amundson at collins dot com
Contributors
-
Isaac Amundson
-
Junaid Babar
-
Karl Hoech
References
-
Tahat, A., Hardin, D., Petz, A., & Alexander, P. (2024). Proof Repair Utilizing Large Language Models: A Case Study on the Copland Remote Attestation Proofbase. Bridging the Gap Between AI and Reality (AISoLA 2024). Springer Nature Switzerland. Retrieved from https://doi.org/10.1007/978-3-031-75434-0_10 (Original work published December 2024)
-
Amundson, I., Cofer, D., Hardin, D., & Hatcliff, J. (2024). Hierarchical Assurance Patterns for Cyber-Resilient Systems Engineering. In 2024 AIAA DATC/IEEE 43rd Digital Avionics Systems Conference (DASC) (pp. 1–9). http://doi.org/10.1109/DASC62030.2024.10748894
-
Mercer, E., Slind, K., Amundson, I., Cofer, D. D., Babar, J., & Hardin, D. (2023). Synthesizing verified components for cyber assured systems engineering. Software and Systems Modeling, 22(1471). http://doi.org/https://doi.org/10.1007/s10270-023-01096-3
-
Amundson, I. (2023). Checking Compliance of AADL Models with Modeling Guidelines using Resolint. SAE International Journal of Advances and Current Practices in Mobility-V132-99EJ. http://doi.org/https://doi.org/10.4271/2023-01-0995
-
Belt, J., Hatcliff, J., , Shackleton, J., Carciofini, J., Carpenter, T., … Mcleod, K. (2023). Model-driven development for the seL4 microkernel using the HAMR framework. Journal of Systems Architecture, 134, 102789. http://doi.org/https://doi.org/10.1016/j.sysarc.2022.102789
-
Hardin, D. (2023). Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero Trust Architecture Development. Ada Lett., 42, 55–61. http://doi.org/10.1145/3591335.3591340 (Original work published December 2022)
-
Belt, J., Hatcliff, J., , Shackleton, J., Carciofini, J., Carpenter, T., … Mcleod, K. (2023). Model-driven development for the seL4 microkernel using the HAMR framework. Journal of Systems Architecture, 134, 102789. http://doi.org/https://doi.org/10.1016/j.sysarc.2022.102789
-
Hardin, D. (2022). Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. Electronic Proceedings in Theoretical Computer Science, 359. http://doi.org/10.4204/eptcs.359.16
-
Cofer, D., Amundson, I., Babar, J., Hardin, D., Slind, K., Alexander, P., … Shackleton, J. (2022). Cyber Assured Systems Engineering at Scale. IEEE Security & Privacy, 20, 52–64. http://doi.org/10.1109/MSEC.2022.3151733
-
Liu, C., Cofer, D. D., & Mercer, E. (2022). Assume-Guarantee Reasoning with Scheduled Components. In J. Babar, I. Amundson, & K. Hoech (Eds.), NASA Formal Methods (pp. 355–372). Springer Nature Switzerland. http://doi.org/10.1007/978-3-031-06773-0_19
-
Mercer, E., Slind, K., Amundson, I., Cofer, D. D., Babar, J., & Hardin, D. (2021). Synthesizing Verified Components for Cyber Assured Systems Engineering. Model-Driven Engineering Languages and Systems (MODELS). Retrieved from https://loonwerks.com/publications/pdf/mercer2021MODELS.pdf (Original work published October 2021)
-
Slind, K. (2021). Specifying Message Formats with Contiguity Types. In L. Cohen & C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving (ITP 2021) (Vol. 193, pp. 1–30). Dagstuhl, Germany: Schloss Dagstuhl — Leibniz-Zentrum für Informatik. http://doi.org/10.4230/LIPIcs.ITP.2021.30
-
Backes, J., Cofer, D. D., & Amundson, I. (2021). The Assume Guarantee Reasoning Environment with Application to an Unmanned Helicopter (p. 16). Retrieved from https://loonwerks.com/publications/pdf/backes2021techreport.pdf
-
Amundson, I., & Cofer, D. (2021). Resolute assurance arguments for cyber assured systems engineering. In Proceedings of the Workshop on Design Automation for CPS and IoT (pp. 7–12). New York, NY, USA: Association for Computing Machinery. http://doi.org/10.1145/3445034.3460507
-
Hardin, D., & Slind, K. (2021). Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations. In 2021 IEEE Security and Privacy Workshops (SPW) (pp. 111–120). http://doi.org/10.1109/SPW53761.2021.00024
-
Hardin, D. (2020). Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems. In 2020 IEEE International Systems Conference (SysCon) (pp. 1–6). http://doi.org/10.1109/SysCon47679.2020.9381831
-
Hardin, D. (2020). Put Me on the RAC. Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2’20). G. Passmore, R. Gamboa. Retrieved from https://loonwerks.com/publications/pdf/hardin2020acl2.pdf
-
Hardin, D., Slind, K., Pohjola, J. A., & Sproul, M. (2020). Synthesis of Verified Architectural Components for Critical Systems Hosted on a Verified Microkernel. 53rd Hawaii International Conference on System Sciences. Retrieved from https://loonwerks.com/publications/pdf/hardin2020icss.pdf (Original work published January 2020)