Radboud Repository

      View Item 
      •   Radboud Repository
      • Collections Radboud University
      • Datasets
      • View Item
      •   Radboud Repository
      • Collections Radboud University
      • Datasets
      • View Item
      JavaScript is disabled for your browser. Some features of this site may not work without it.
      BrowseAll of RepositoryCollectionsDepartmentsDate IssuedAuthorsTitlesDocument typeThis CollectionDepartmentsDate IssuedAuthorsTitlesDocument type
      StatisticsView Item Statistics

      Formal Specification of a Generic Separation Kernel

      Find Full text
      Creators
      Verbeek, F.
      Tverdyshev, S.
      Havle, O.
      Blasum, H.
      Langenstein, B.
      Stephan, W.
      Nemouchi, Y.
      Feliachi, A.
      Wolff, B.
      Schmaltz, J.
      Date of Archiving
      2014
      Archive
      Archive of Formal Proofs
      Related links
      http://afp.sourceforge.net/entries/CISC-Kernel.shtml
      Publication type
      Dataset
      Access level
      Open access
      Please use this identifier to cite or link to this item: https://hdl.handle.net/2066/151883   https://hdl.handle.net/2066/151883
      Display more detailsDisplay less details
      Organization
      Software Science
      Audience(s)
      Astronomy, astrophysics
      Key words
      Intransitive noninterference; Generic Separation Kernel
      Abstract
      Intransitive noninterference has been a widely studied topic in the last few decades. Several well-established methodologies apply interactive theorem proving to formulate a noninterference theorem over abstract academic models. In joint work with several industrial and academic partners throughout Europe, we are helping in the certification process of PikeOS, an industrial separation kernel developed at SYSGO. In this process, established theories could not be applied. We present a new generic model of separation kernels and a new theory of intransitive noninterference. The model is rich in detail, making it suitable for formal verification of realistic and industrial systems such as PikeOS. Using a refinement-based theorem proving approach, we ensure that proofs remain manageable.
      This item appears in the following Collection(s)
      • Datasets [1609]
      • Faculty of Science [34584]
       
      •  Upload Full Text
      •  Terms of Use
      •  Notice and Takedown
      Bookmark and Share
      Admin login