The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
This paper presents a technique for specifying and reasoning about the operational semantics of distributed programming languages. We formalize the concept of “vertical stacking” of distributed systems, an extension of Joyce's, Windley's and Curzon's stacking methodologies for sequential systems and of the CLI “short stack” which stacks interpreters for object code, assembly code, and a high-level...
A compositional proof method allows the components of a system to be specified and verified independently, instead of having to verify the entire system as a monolithic unit. This paper describes how the composition principle of Abadi and Lamport can be applied to specify and compose systems that consist of both safety and progress properties, using the HOL theorem proving system. We discuss the translation...
This paper presents our current effort to formally derive, using HOL, a sound Hoare logic for the concurrent programming language microSR, a derivative of SR. Our methodology is built on Gordon's work on mechanizing programming logics for a small sequential programming language. The constructs of microSR include those basic to common sequential programming languages, in addition to an asynchronous...
Contemporary cloud environments are built on low-assurance components, so they cannot provide a high level of assurance about the isolation and protection of information. A “multi-level” secure cloud environment thus typically consists of multiple, isolated clouds, each of which handles data of only one security level. Not only are such environments duplicative and costly, data “sharing” must be implemented...
Although one senior security professional has emphasized that “it is unconscionable to use overly weak components” in a multilevel security (MLS) context, the majority of current transfer guards do exactly that. Basic guard technology is well-developed and has a long history, but most guards are built on low-assurance systems vulnerable to software subversion, and the lack of assurance limits the...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.