THREAD ALGEBRA FOR NONINTERFERENCE

Th read algeb r a is a sem ant ics for recent ob ject - orient e dp r ogram m in g lan gu ages [J.A . Bergst ra an d M.E. L o ot s, J. Logi c Al gebr.Program. 51 ( 2002) 125–156; J.A . Bergst ra an d C.A . Mid d e lb u r g,Fo rm al Aspects C om put. ( 2007) ] s u ch as C# an d Java. Th i s p ap ersh ows t hat t hread algeb ra prov id es a p ro cess- algebraic framework forreason in g ab ou t an d c lassify in g variou s st an d ard n ot ion s of n on int e r-ference, an imp ortant p rop erty in secure information flow. We willt ake t h e n on int e rferen ce p r op erty give n by Volp an oet al . [D . Volpano,G. Smith and C. Irvine, J. Com p ut. S ecur. 4 ( 1996) 167–187] on ty p esy stems as an example of ou r approach. We define a comparable n o-t ion of n on int erferen c e in t h e set t in g of t h read algeb r a. O u r ap p r oachgives a similar result to the approach of [G. Smith and D. Volp an o, inPOPL’ 9829( 1998) 355–364] an d c an b e ap p lied t o u n s t r u c t u red an dmu ltithreaded p rogramming languages