vault backup: 2025-01-22 10:13:09

201 Metadata/My Library.bib

@@ -1410,6 +1410,24 @@ Opportunities and Challenges toward Responsible AI.pdf}
   file = {/home/danesabo/Zotero/storage/DIDSY7TD/Biggs - 1996 - Enhancing teaching through constructive alignment.pdf}
 }
 
+@inproceedings{biggsJuryMonolithicOS2018,
+  title = {The {{Jury Is In}}: {{Monolithic OS Design Is Flawed}}: {{Microkernel-based Designs Improve Security}}},
+  shorttitle = {The {{Jury Is In}}},
+  booktitle = {Proceedings of the 9th {{Asia-Pacific Workshop}} on {{Systems}}},
+  author = {Biggs, Simon and Lee, Damon and Heiser, Gernot},
+  date = {2018-08-27},
+  pages = {1--7},
+  publisher = {ACM},
+  location = {Jeju Island Republic of Korea},
+  doi = {10.1145/3265723.3265733},
+  url = {https://dl.acm.org/doi/10.1145/3265723.3265733},
+  urldate = {2025-01-22},
+  eventtitle = {{{APSys}} '18: 9th {{Asia-Pacific Workshop}} on {{Systems}}},
+  isbn = {978-1-4503-6006-7},
+  langid = {english},
+  file = {/home/danesabo/Zotero/storage/KIMYMDUA/Biggs et al. - 2018 - The Jury Is In Monolithic OS Design Is Flawed Microkernel-based Designs Improve Security.pdf}
+}
+
 @article{blanchiniModelFreePlantTuning2017,
   title = {Model-{{Free Plant Tuning}}},
   author = {Blanchini, Franco and Fenu, Gianfranco and Giordano, Giulia and Pellegrino, Felice Andrea},
@@ -4278,6 +4296,25 @@ Artificial Intelligence Program.pdf}
   file = {/home/danesabo/Zotero/storage/JF5DILLS/Fisher et al. - 2017 - The HACMS program using formal methods to elimina.pdf}
 }
 
+@article{fisherHACMSProgramUsing2017a,
+  title = {The {{HACMS}} Program: Using Formal Methods to Eliminate Exploitable Bugs},
+  shorttitle = {The {{HACMS}} Program},
+  author = {Fisher, Kathleen and Launchbury, John and Richards, Raymond},
+  date = {2017-10-13},
+  journaltitle = {Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences},
+  shortjournal = {Phil. Trans. R. Soc. A.},
+  volume = {375},
+  number = {2104},
+  pages = {20150401},
+  issn = {1364-503X, 1471-2962},
+  doi = {10.1098/rsta.2015.0401},
+  url = {https://royalsocietypublishing.org/doi/10.1098/rsta.2015.0401},
+  urldate = {2025-01-22},
+  abstract = {For decades, formal methods have offered the promise of verified software that does not have exploitable bugs. Until recently, however, it has not been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. Its designers proved it to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and guaranteeing integrity and confidentiality. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution, including faster processors, increased automation, more extensive infrastructure, specialized logics and the decision to co-develop code and correctness proofs rather than verify existing artefacts. In this paper, we explore the promise and limitations of current formal-methods techniques. We discuss these issues in the context of DARPA’s HACMS program, which had as its goal the creation of high-assurance software for vehicles, including quadcopters, helicopters and automobiles.             This article is part of the themed issue ‘Verified trustworthy software systems’.},
+  langid = {english},
+  file = {/home/danesabo/Zotero/storage/RJ2PKUDM/Fisher et al. - 2017 - The HACMS program using formal methods to eliminate exploitable bugs.pdf}
+}
+
 @inproceedings{fitzgeraldCyberPhysicalSystemsDesign2015,
   title = {Cyber-{{Physical Systems Design}}: {{Formal Foundations}}, {{Methods}} and {{Integrated Tool Chains}}},
   shorttitle = {Cyber-{{Physical Systems Design}}},