{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:52Z","timestamp":1761596932790},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291060"},{"type":"electronic","value":"9783540320241"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560586_29","type":"book-chapter","created":{"date-parts":[[2005,10,20]],"date-time":"2005-10-20T14:08:27Z","timestamp":1129817307000},"page":"360-374","source":"Crossref","is-referenced-by-count":22,"title":["A Typed Assembly Language for Non-interference"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Medel","sequence":"first","affiliation":[]},{"given":"Adriana","family":"Compagnoni","sequence":"additional","affiliation":[]},{"given":"Eduardo","family":"Bonelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3-4","key":"29_CR1","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1023\/B:JARS.0000021014.79255.33","volume":"31","author":"D. Aspinall","year":"2003","unstructured":"Aspinall, D., Compagnoni, A.B.: Heap bounded assembly language. Journal of Automated Reasoning, Special Issue on Proof-Carrying Code\u00a031(3-4), 261\u2013302 (2003)","journal-title":"Journal of Automated Reasoning, Special Issue on Proof-Carrying Code"},{"key":"29_CR2","unstructured":"Banerjee, A., Naumann, D.: Secure information flow and pointer confinement in a java-like language. In: Proceedings of Fifteenth IEEE Computer Security Foundations - CSFW, June 2002, pp. 253\u2013267 (2002)"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-24622-0_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Basu, A., Rezk, T.: Security types preserving compilation. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 2\u201315. Springer, Heidelberg (2004)"},{"key":"29_CR4","unstructured":"Bell, D., LaPadula, L.: Secure computer systems: Mathematical foundations and model. Technical Report Technical Report MTR 2547 v2, MITRE (November 1973)"},{"key":"29_CR5","unstructured":"Biba, K.: Integrity considerations for secure computer systems. Technical Report ESD-TR-76-372, USAF Electronic Systems Division, Bedford, MA (April 1977)"},{"key":"29_CR6","unstructured":"Crary, K., Kliger, A., Pfenning, F.: A monadic analysis of information flow security with mutable state. Technical Report CMU-CS-03-164, Carnegie Mellon University (September 2003)"},{"issue":"7","key":"29_CR7","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D.E. Denning","year":"1977","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Communications of the ACM"},{"issue":"5","key":"29_CR8","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D.E. Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Communications of the ACM\u00a019(5), 236\u2013242 (1976)","journal-title":"Communications of the ACM"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Feiertag, R.J., Levitt, K.N., Robinson, L.: Proving multilevel security of a system design. In: 6th ACM Symp. Operating System Principles, November 1977, pp. 57\u201365 (1977)","DOI":"10.1145\/800214.806547"},{"key":"29_CR10","first-page":"11","volume-title":"Proceedings of the Symposium on Security and Privacy","author":"J.A. Goguen","year":"1982","unstructured":"Goguen, J.A., Meseguer, J.: Security policy and security models. In: Proceedings of the Symposium on Security and Privacy, pp. 11\u201320. IEEE Press, Los Alamitos (1982)"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"Hedin, D., Sands, D.: Timing aware information flow security for a javacard-like bytecode. In: Proceedings of BYTECODE, ETAPS 2005 (2005) (to appear)","DOI":"10.1016\/j.entcs.2005.02.031"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-44585-4_26","volume-title":"Computer Aided Verification","author":"X. Leroy","year":"2001","unstructured":"Leroy, X.: Java bytecode verification: an overview. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 265\u2013285. Springer, Heidelberg (2001)"},{"key":"29_CR13","unstructured":"Medel, R., Compagnoni, A., Bonelli, E.: A typed assembly language for secure information flow analysis (2005), http:\/\/www.cs.stevens.edu\/~rmedel\/hbal\/publications\/sifTechReport.ps"},{"issue":"3","key":"29_CR14","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to Typed Assembly Language. ACM Transactions on Programming Languages and Systems\u00a021(3), 528\u2013569 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Types in Compilation","author":"G. Morrisett","year":"1998","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Leroy, X., Ohori, A. (eds.) TIC 1998. LNCS, vol.\u00a01473, pp. 28\u201352. Springer, Heidelberg (1998)"},{"key":"29_CR16","unstructured":"Necula, G.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (September 1998)"},{"key":"29_CR17","first-page":"421","volume-title":"Proceedings of the 2nd International Conference on Software Engineering","author":"P.G. Neumman","year":"1976","unstructured":"Neumman, P.G., Feiertag, R.J., Levitt, K.N., Robinson, L.: Software development and proofs of multi-level security. In: Proceedings of the 2nd International Conference on Software Engineering, pp. 421\u2013428. IEEE Computer Society Press, Los Alamitos (1976)"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications\u00a021(1) (2003)","DOI":"10.1109\/JSAC.2002.806121"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 366\u2013381. Springer, Heidelberg (2000)"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Volpano, D.M., Smith, G.: A type-based approach to program security. In: TAPSOFT, pp. 607\u2013621 (1997)","DOI":"10.21236\/ADA486429"},{"key":"29_CR21","unstructured":"Xi, H., Harper, R.: A dependently typed assembly language. Technical Report OGI-CSE-99-008, Oregon Graduate Institute of Science and Technology (July 1999)"},{"key":"29_CR22","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.: Secure information flow via linear continuations. Higher Order and Symbolic Computation\u00a015(2\u20133) (2002)","DOI":"10.1023\/A:1020843229247"}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560586_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:50:35Z","timestamp":1605642635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560586_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291060","9783540320241"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11560586_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}