{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T16:52:34Z","timestamp":1781110354977,"version":"3.54.1"},"reference-count":28,"publisher":"IGI Global Scientific Publishing","issue":"3","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,7]]},"abstract":"<jats:p>Multi-million gate system-on-chip (SoC) designs easily fit into today\u2019s Field Programmable Gate Arrays (FPGAs). As FPGAs become more common in safety-critical and mission-critical systems, researchers and designers require information flow guarantees for the FPGAs. Tools for designing a secure system of chips (SOCs) using FPGAs and new techniques to manage and analyze the security properties precisely are desirable. In this work we propose a formal approach to model, analyze and verify a typical set of security properties \u2013 noninterference \u2013 of Handel C programs using Petri Nets and model checking. This paper presents a method to model Handel C programs using Predicate Transition Nets, a type of Petri Net, and define security properties on the model, plus a verification approach where security properties are checked. Three steps are used. First, a formal specification on the Handel C description using Petri Nets is extracted. Second, the dynamic noninterference properties with respect to the Handel C program statements are defined on the model. To assist in verification, a translation rule from the Petri Nets specification to the Maude programming language is also defined. Thus, the formal specification can be verified against the system properties using model checking. A case study of the pipeline multiplier is discussed to illustrate the concept and validate the approach.<\/jats:p>","DOI":"10.4018\/jsse.2012070103","type":"journal-article","created":{"date-parts":[[2012,11,26]],"date-time":"2012-11-26T14:06:12Z","timestamp":1353938772000},"page":"50-65","source":"Crossref","is-referenced-by-count":0,"title":["Formal Modeling and Verification of Security Property in Handel C Program"],"prefix":"10.4018","volume":"3","author":[{"given":"Yujian","family":"Fu","sequence":"first","affiliation":[{"name":"Alabama A&M University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeffery","family":"Kulick","sequence":"additional","affiliation":[{"name":"University of Alabama in Huntsville, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lok K.","family":"Yan","sequence":"additional","affiliation":[{"name":"Air Force Research Laboratory, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steven","family":"Drager","sequence":"additional","affiliation":[{"name":"Air Force Research Laboratory, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"jsse.2012070103-0","author":"E.Albrechtsen","year":"2002","journal-title":"Risk and vulnerability: A generic comparison of industrial safety and information security"},{"key":"jsse.2012070103-1","unstructured":"Anonymous. (2005) Handel-C user reference manual. London, UK: Celoxica. Retrieved from http:\/\/babbage.cs.qc.edu\/courses\/cs345\/Manuals\/HandelC.pdf"},{"key":"jsse.2012070103-2","doi-asserted-by":"crossref","unstructured":"Chien, A. A., & Byun, J. (1999). Safe and protected execution for the morph\/amrm reconfigurable processor. In Proceedings of the Seventh Annual IEEE Symposium on Field-Programmable Custom Computing Machines (pp. 209-221).","DOI":"10.1109\/FPGA.1999.803683"},{"issue":"2","key":"jsse.2012070103-3","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","article-title":"Maude: Specification and programming in rewriting logic.","volume":"285","author":"M.Clavel","year":"2002","journal-title":"Theoretical Computer Science"},{"key":"jsse.2012070103-4","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., & Talcott, C. (2004). Maude manual. Retrieved from http:\/\/maude.cs.uiuc.edu\/maude2-manual\/maude-manual.pdf"},{"key":"jsse.2012070103-5","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S1571-0661(04)00034-9","article-title":"Principles of Maude.","volume":"4","author":"M.Clavel","year":"1996","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"jsse.2012070103-6","author":"R.Dubey","year":"2008","journal-title":"Introduction to embedded system design using field programmable gate arrays"},{"key":"jsse.2012070103-7","doi-asserted-by":"crossref","unstructured":"Fu, Y., Dong, Z., & He, X. (2006). An approach to Web services oriented modeling and validation. In Proceedings of the 28th ICSE Workshop on Service Oriented Software Engineering (pp. 81-87).","DOI":"10.1145\/1138486.1138504"},{"key":"jsse.2012070103-8","doi-asserted-by":"crossref","unstructured":"Fu, Y., Dong, Z., & He, X. (2006). Modeling, validating and automating composition of Web services. In Proceedings of the Sixth International Conference on Web Engineering (pp. 217-224).","DOI":"10.1145\/1145581.1145626"},{"issue":"6","key":"jsse.2012070103-9","first-page":"1","article-title":"A translator of software architecture design from sam to java.","volume":"17","author":"Y.Fu","year":"2007","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"jsse.2012070103-10","author":"S.Ghosh","year":"1999","journal-title":"Hardware description languages: Concepts and principles"},{"key":"jsse.2012070103-11","doi-asserted-by":"crossref","unstructured":"Gogniat, G., Wolf, T., & Burleson, W. (2006). Reconfigurable security support for embedded systems. In Proceedings of the 39th Annual Hawaii International Conference on System Sciences (p. 250.1).","DOI":"10.1109\/HICSS.2006.409"},{"key":"jsse.2012070103-12","author":"M. J. C.Gordon","year":"1993","journal-title":"Introduction to HOL \u2013 A theorem-proving environment for higher-order logic"},{"key":"jsse.2012070103-13","doi-asserted-by":"crossref","unstructured":"He, X., Ding, J., & Deng, Y. (2002). Model checking software architecture specifications in sam. In Proceedings of the 14th International Conference on Software Engineering and Knowledge Engineering (pp. 271-274).","DOI":"10.1145\/568760.568808"},{"key":"jsse.2012070103-14","author":"C. A. R.Hoare","year":"1985","journal-title":"Communicating sequential processes"},{"key":"jsse.2012070103-15","unstructured":"Holbrook, D. (2001). FPGA use for safety critical functions in an air intercept missile. In Proceedings of the 19th International System Safety Conference (pp. 618-628)."},{"key":"jsse.2012070103-16","doi-asserted-by":"crossref","unstructured":"Huffmire, T., Brotherton, B., Wang, G., Sherwood, T., Kastner, R., & Levin, T. \u2026Irvine, C. (2007). Moats and drawbridges: An isolation primitive for reconfigurable hardware based systems. In Proceedings of the IEEE Symposium on Security and Privacy (pp. 281-295).","DOI":"10.1109\/SP.2007.28"},{"key":"jsse.2012070103-17","unstructured":"Huffmire, T., Prasad, S., Sherwood, T., & Kastner, R. (2006). Policy-driven memory protection for reconfigurable systems. In Proceedings of the European Symposium on Research in Computer Security."},{"key":"jsse.2012070103-18","unstructured":"Katz, R. (2000). Faster, better, cheaper space flight electronics \u2013 an analytical case study. In Proceedings of the Conference on Mil\/Aero Applications of Programmable Logic Devices."},{"key":"jsse.2012070103-19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","author":"Z.Manna","year":"1992","journal-title":"The temporal logic of reactive and concurrent systems"},{"issue":"1","key":"jsse.2012070103-20","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency.","volume":"96","author":"J.Meseguer","year":"1992","journal-title":"Theoretical Computer Science"},{"key":"jsse.2012070103-21","doi-asserted-by":"crossref","unstructured":"Meseguer, J. (1998, June). Membership algebra as a logical framework for equational specification. In F. P. Presicce (Eds.), Proceedings of the Workshop on Algebraic Development Techniques (LNCS 1376, pp. 18-61).","DOI":"10.1007\/3-540-64299-4_26"},{"issue":"4","key":"jsse.2012070103-22","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","article-title":"Petri Nets: Properties, analysis and applications.","volume":"77","author":"T.Murata","year":"1989","journal-title":"Proceedings of the IEEE"},{"key":"jsse.2012070103-23","doi-asserted-by":"crossref","unstructured":"Pnueli, A. (1977). The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science (pp. 46-57).","DOI":"10.1109\/SFCS.1977.32"},{"key":"jsse.2012070103-24","author":"A. N.Prior","year":"1979","journal-title":"Temporal logic of reactive and concurrent systems"},{"issue":"2","key":"jsse.2012070103-25","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s10515-005-6205-y","article-title":"Rewriting-based techniques for runtime verification.","volume":"12","author":"G.Rosu","year":"2004","journal-title":"Journal of Automated Software Engineering"},{"key":"jsse.2012070103-26","doi-asserted-by":"crossref","unstructured":"Shivakumar, P., Kistler, M., Keckler, S. W., Burger, D., Alvisi, L., & Technical, I. \u2026Rajamony, R. (2002, June). Modeling the effect of technology trends on the soft error rate of combinational logic. In Proceedings of the International Conference on the Dependable Systems and Networks (pp. 389-398).","DOI":"10.1109\/DSN.2002.1028924"},{"key":"jsse.2012070103-27","unstructured":"Vickery, C. (2003). Sample Handel C code. Retrieved from http:\/\/babbage.cs.qc.edu\/courses\/cs345\/2003_09\/Sample_Code\/html\/pipe mult.hcc.html"}],"container-title":["International Journal of Secure Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=69393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,5]],"date-time":"2019-07-05T23:58:21Z","timestamp":1562371101000},"score":1,"resource":{"primary":{"URL":"http:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/jsse.2012070103"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":28,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.4018\/jsse.2012070103","relation":{},"ISSN":["1947-3036","1947-3044"],"issn-type":[{"value":"1947-3036","type":"print"},{"value":"1947-3044","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}