{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:00:50Z","timestamp":1777806050237,"version":"3.51.4"},"reference-count":41,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2018,4,4]],"date-time":"2018-04-04T00:00:00Z","timestamp":1522800000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2018,4,9]]},"abstract":"<jats:p>We present a new algorithm, together with a full soundness proof, which guarantees probabilistic noninterference (PN) for concurrent programs. The algorithm follows the \u201clow-deterministic security\u201d (LSOD) approach, but for the first time allows general low-nondeterminism as long as PN is not violated.<\/jats:p>\n                  <jats:p>The algorithm is based on the earlier observation by Giffhorn and Snelting that low-nondeterminism is secure as long as it is not influenced by high events [ International Journal of Information Security 14 ( 2015 ) 263\u2013287]. It uses a new system of classification flow equations in multi-threaded programs, together with inter-thread\/interprocedural dominators. Compared to LSOD, precision is boosted and false alarms are minimized. We explain details of the new algorithm and its soundness proof.<\/jats:p>\n                  <jats:p>The algorithm is integrated into the JOANA software security tool, and can handle full Java with arbitrary threads. We apply JOANA to a multi-threaded e-voting system, and show how the algorithm eliminates false alarms. We thus demonstrate that low-deterministic security is a highly precise and practically mature software security analysis method.<\/jats:p>","DOI":"10.3233\/jcs-17984","type":"journal-article","created":{"date-parts":[[2018,4,6]],"date-time":"2018-04-06T11:21:27Z","timestamp":1523013687000},"page":"335-366","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":5,"title":["Low-deterministic security for low-nondeterministic programs"],"prefix":"10.1177","volume":"26","author":[{"given":"Simon","family":"Bischof","sequence":"first","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Breitner","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Graf","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hecker","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Mohr","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gregor","family":"Snelting","sequence":"additional","affiliation":[{"name":"Karlsruhe Institute of Technology, Germany. E-mail:\u00a0"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2018,4,4]]},"reference":[{"key":"ref001","doi-asserted-by":"crossref","unstructured":"W.\u00a0Ahrendt, B.\u00a0Beckert, R.\u00a0Bubel, R.\u00a0H\u00e4hnle, P.H.\u00a0Schmitt and M.\u00a0Ulbrich (eds), Deductive Software Verification\u00a0\u2013 the Key Book\u00a0\u2013 from Theory to Practice, Lecture Notes in Computer Science, Vol.\u00a010001, Springer, 2016.","DOI":"10.1007\/978-3-319-49812-6"},{"key":"ref002","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88313-5_22"},{"key":"ref003","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"ref004","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49635-0_4"},{"key":"ref005","doi-asserted-by":"publisher","DOI":"10.1145\/1255450.1255452"},{"key":"ref006","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-010-9114-7"},{"key":"ref007","unstructured":"D.\u00a0Giffhorn, Slicing of Concurrent Programs and its Application to Information Flow Control, PhD thesis, Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik, 2012."},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-014-0257-6"},{"key":"ref009","unstructured":"J.\u00a0Graf, Information Flow Control with System Dependence Graphs \u2014 Improving Modularity, Scalability and Precision for Object Oriented Languages, PhD thesis, Karlsruher Institut f\u00fcr Technologie, Fakult\u00e4t f\u00fcr Informatik, 2016."},{"key":"ref010","unstructured":"J.\u00a0Graf, M.\u00a0Hecker, M.\u00a0Mohr and G.\u00a0Snelting, Checking applications using security APIs with JOANA, 2015, 8th International Workshop on Analysis of Security APIs."},{"key":"ref011","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49635-0_5"},{"key":"ref012","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66197-1_19"},{"key":"ref013","doi-asserted-by":"crossref","unstructured":"C.\u00a0Hammer, Experiences with PDG-based IFC, in: Proc. ESSoS\u201910, F.\u00a0Massacci, D.\u00a0Wallach and N.\u00a0Zannone, eds, LNCS, Vol.\u00a05965, Springer-Verlag, 2010, pp.\u00a044\u201360.","DOI":"10.1007\/978-3-642-11747-3_4"},{"key":"ref014","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-009-0086-1"},{"key":"ref015","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73573"},{"key":"ref016","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31762-0_12"},{"key":"ref017","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.6"},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111045"},{"key":"ref019","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_12"},{"key":"ref020","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.28"},{"key":"ref021","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.9"},{"key":"ref022","doi-asserted-by":"publisher","DOI":"10.1007\/11532378_15"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-27436-2_12"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.22"},{"key":"ref025","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15497-3_8"},{"key":"ref026","unstructured":"M.\u00a0Mohr, J.\u00a0Graf and M.\u00a0Hecker, JoDroid: Adding Android support to a static information flow control tool, in: Gemeinsamer Tagungsband der Workshops der Tagung Software Engineering 2015, Dresden, Germany, 17.\u201318. M\u00e4rz 2015, CEUR Workshop Proceedings, Vol.\u00a01337, CEUR-WS.org, 2015, pp.\u00a0140\u2013145."},{"key":"ref027","doi-asserted-by":"publisher","DOI":"10.1145\/288195.288213"},{"key":"ref028","unstructured":"T.M.\u00a0Ngo, Qualitative and quantitative information flow analysis for multi-threaded programs, PhD thesis, University of Enschede, 2014."},{"key":"ref029","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_17"},{"key":"ref030","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_18"},{"key":"ref031","doi-asserted-by":"crossref","unstructured":"T.\u00a0Reps, S.\u00a0Horwitz, M.\u00a0Sagiv and G.\u00a0Rosay, Speeding up slicing, in: Proc. FSE \u201994, ACM, New York, NY, USA, 1994, pp.\u00a011\u201320.","DOI":"10.1145\/193173.195287"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"A.W.\u00a0Roscoe, J.\u00a0Woodcock and L.\u00a0Wulf, Non-interference through determinism, in: ESORICS, LNCS, Vol.\u00a0875, 1994, pp.\u00a033\u201353.","DOI":"10.1007\/3-540-58618-0_55"},{"key":"ref033","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref034","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2000.856937"},{"key":"ref035","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2006-14605"},{"key":"ref036","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268975"},{"key":"ref037","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61739-6_51"},{"key":"ref038","doi-asserted-by":"publisher","DOI":"10.1515\/itit-2014-1051"},{"key":"ref039","doi-asserted-by":"publisher","DOI":"10.1145\/1178625.1178628"},{"key":"ref040","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554345"},{"key":"ref041","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-17984","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-17984","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-17984","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:12Z","timestamp":1777495512000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-17984"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,4]]},"references-count":41,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,4,9]]}},"alternative-id":["10.3233\/JCS-17984"],"URL":"https:\/\/doi.org\/10.3233\/jcs-17984","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,4,4]]}}}