Developing Safe Software with Modular Behavioral Properties (단위별 행위특성을 이용한 안전한 소프트웨어 개발)

Hyongsoon Kim (김형순); Eunyoung Lee (이은영)

Developing Safe Software with Modular Behavioral Properties

Journal of Knowledge Information Technology and Systems
Abbr : JKITS
2010, 5(5), pp.101-110
Publisher : Korea Knowledge Information Technology Society
Research Area : Interdisciplinary Studies > Interdisciplinary Research
Published : October 31, 2010

Hyongsoon Kim ¹, Eunyoung Lee ²

¹한국정보화진흥원
²동덕여자대학교

Candidate

ABSTRACT

Verifying software components before deploying them is a significant process when component-based software development is considered for building a large-scale software system. In this paper, we propose a refined model of "property" of Secure Linking (SLinking) and SL-JML using the new model. SL-JML is a behavioral specification language based on the Secure Linking framework, which inter-operates with JML specification. We also show that SL-JML is more flexible than previous JML specifications without compromising the expressive power of the essence of JML specification.

KEYWORDS

software verification, software component, code security, formal specification

Citation status

* References for papers published after 2023 are currently being built.

[book] T. Gilb / 1993 / Software Inspection, chapter 19 / Addison-Wesley

[confproc] Eunyoung Lee / 2003 / Policy-enforced linking of untrusted components (extended abstract) / Proceedings of the 9th European Software Engineering Conference and the 10th ACM SIGSOFT International Symposium on the Foundations of Software Engineering

[journal] K. Apt / 1981 / Ten years of hoare's logic: A survey (part I) / ACM Transactions on Programming Languages and Systems 3(4) : 431~483

[journal] Barbara H. Liskov / 1994 / A behavioral notion of subtyping / ACM Transactions on Programming Languages and Systems 16(6) : 1811~1841

[journal] Amy Moormann Zaremski / 1997 / Specification matching of software components / ACM Trans. Softw. Eng. Methodol 6(4) : 333~369

[journal] Jeannette M. Wing / 1987 / Writing larch interface language specifications / ACM Trans. Program. Lang. Syst. 9(1) : 1~24

[thesis] Eunyoung Lee / 2004 / Secure Linking: a Logical Framework for Policy-Enforced Component Composition / 박사 / Princeton University

[book] Andrew W. Appel / 2000 / A semantic model of types and machine instructions for proof-carrying code / POPL : 243~253

[confproc] Andrew W. Appel / 2001 / Foundational proof-carrying code / 16th Annual IEEE Symposium on Logic in Computer Science

[confproc] Andrew W. Appel / 1999 / Proof-carrying authentication / 6th ACM Conference on Computer and Communications Security

[book] Gary T. Leavens / 1999 / JML: A notation for detailed design, 1999. adapted from Behavioral specifications for Businesses and Systems. Chapter 12 : 175~188

[book] Gary T. Leavens / Larch/C++ Reference Manual Version 5.14

[book] K. Rustan / 2000 / ESC/Java User's Manual / Compaq Systems Research Center

[web] Microsoft / Signing and Checking code with Authenticode / http://msdn.microsoft.com/workshop/security/authcode/signing

[report] VeriSign / 2001 / Code signing digital ids for sun java signing. Technical report / VeriSign

[confproc] G. C. Necula / 1997 / Proof-carrying code / Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL '97)

[confproc] G. C. Necula / 2002 / Ccured: Type-safe retrotting of legacy code / Twenty-Ninth ACM Symposium on Principles of Programming Languages

[confproc] Neal Glew / 1999 / Type-safe linking and modular assembly language / Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages : 250~261

[confproc] Greg Morrisett / 1998 / From system f to typed assembly language / Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages : 85~97

[book] Frank Pfenning and Carsten Schuurmann / 2002 / Twelf User's Guide, Version 1.4

KJCKorea
Journal Central

Journal of Knowledge Information Technology and Systems 2023 KCI Impact Factor : 0.89