Diff of /web/entries/Strong_Security.shtml [851132] .. [0bfa2c]  Maximize  Restore

Switch to side-by-side view

--- a/web/entries/Strong_Security.shtml
+++ b/web/entries/Strong_Security.shtml
@@ -27,15 +27,14 @@
 <h1><font class="first">A</font>
 <font class="first">F</font>ormalization
 of
-<font class="first">D</font>eclassification
-with
-<font class="first">W</font>HAT-and-WHERE-Security
+<font class="first">S</font>trong
+<font class="first">S</font>ecurity
 </h1>
 <p></p>
 <table width="80%" class="data">
   <tbody>
     <tr><td class="datahead" width="20%">Title:</td>
-        <td class="data" width="80%">A Formalization of Declassification with WHAT-and-WHERE-Security</td></tr>
+        <td class="data" width="80%">A Formalization of Strong Security</td></tr>
 
     <tr><td class="datahead">Author:</td>
         <td class="data">Sylvia Grewe (grewe /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de), Alexander Lux (lux /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de), Heiko Mantel (mantel /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de) and Jens Sauer (sauer /at/ mais /dot/ informatik /dot/ tu-darmstadt /dot/ de)</td></tr>
@@ -48,21 +47,17 @@
 
 Research in information-flow security aims at developing methods to
 identify undesired information leaks within programs from private
-sources to public sinks. Noninterference captures this intuition by
-requiring that no information whatsoever flows from private sources
-to public sinks. However, in practice this definition is often too
-strict: Depending on the intuitive desired security policy, the
-controlled declassification of certain private information (WHAT) at
-certain points in the program (WHERE) might not result in an
-undesired information leak.
+sources to public sinks. Noninterference captures this
+intuition. Strong security from Sabelfeld and Sands
+formalizes noninterference for concurrent systems.
 <p>
-We present an Isabelle/HOL formalization of such a security property
-for controlled declassification, namely WHAT&WHERE-security from
-"Scheduler-Independent Declassification" by Lux, Mantel, and Perner.
+We present an Isabelle/HOL formalization of strong security for
+arbitrary security lattices (Sabelfeld and Sands use
+a two-element security lattice in the original publication).
 The formalization includes
-compositionality proofs for and a soundness proof for a security
-type system that checks for programs in a simple while language with
-dynamic thread creation.
+compositionality proofs for strong security and a soundness proof
+for a security type system that checks strong security for programs
+in a simple while language with dynamic thread creation.
 <p>
 Our formalization of the security type system is abstract in the
 language for expressions and in the semantic side conditions for
@@ -70,16 +65,13 @@
 approximations for these side conditions. The soundness proof of
 such an instantiation boils down to showing that these syntactic
 approximations imply the semantic side conditions.
-<p>
-This Isabelle/HOL formalization uses theories from the entry
-Strong Security.
         </td></tr>
 
     <tr><td class="datahead" valign="top">BibTeX:</td>
         <td class="formatted">
 			<pre>@article{Strong_Security-AFP,
   author  = {Sylvia Grewe and Alexander Lux and Heiko Mantel and Jens Sauer},
-  title   = {A Formalization of Declassification with WHAT-and-WHERE-Security},
+  title   = {A Formalization of Strong Security},
   journal = {Archive of Formal Proofs},
   month   = apr,
   year    = 2014,

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks