HCSS'12

file

Visible to the public Margrave: Query-Based Policy Analysis

Abstract:

Margrave is a policy-analysis tool providing query-based verification and query-based views of policies. It supports reasoning about the combined effects of policies written in different configuration languages, such as a firewall filter and a static router, or multiple cooperating access-control policies in an enterprise. It supports "change-impact analysis", allowing a user to compare the effects of policy updates.

file

Visible to the public Designed-In Security for Mobile Architectures

Abstract:

Mobile applications--both native and web-based--are a critical emerging segment of the software industry, and security for these applications is of increasing concern. Unfortunately, today's mobile applications are expressed at a low level of abstraction in which important security properties are implicit and only indirectly related to code, making assurance difficult.

file

Visible to the public Lessons from Twenty Years of Industrial Formal Methods

Abstract:

Over the last two decades formal methods have achieved widespread use by industry in the development of safety and security critical systems. However, these successes often go unacknowledged as evidence of the successful transition of formal methods simply because

file

Visible to the public 3 Years After L.4 Verified

In 2009, the L4.verified project delivered a machine-checked, formal proof that the C code of the seL4 microkernel correctly implements its abstract specification. This proof measured roughly 200,00 lines of proof script in the interactive theorem prover Isabelle/HOL. In the years since then, the kernel has been publicly released for evaluation and teaching, has undergone API evolution, and has been even more deeply analyzed, including: