초록

소프트웨어 컴포넌트를 이용하여 시스템을 구성하는 경우 그리 간단하지 않은데, 그것은 링크 과정 자체가 서로 다른 버전들과 디지털 서명, 정적인 타입 정보나 네트워크로 전송된 소프트웨어, 그리고 서로 다른 판매자에 의한 컴포넌트들을 모두 포함하는 복잡한 과정이기 때문이다. 만약 링크과정에 적용될 수 있는 링크 정책을 수립하고 이를 링크 시에 적용할 수 있는 방법이 있다면 이러한 복잡함을 해결하는 좋은 수단이 된다. 시큐어 링킹(Secure Linking)은 사용자가 안전한 링크를 위한 정책을 만들고 이를 링크 시에 적용할 수 있도록 해주는 새로운 링크 프로토콜이며, 시큐어 링크 프레임워크(Secure Linking Framework)는 시큐어 링크 시스템 구현을 위한 논리적 프레임워크이다. 본 논문에서는 시큐어 링크 프레임워크를 이용하여 마이크로 소프트의 닷넷(.NET)에서 사용되는 어셈블리의 링크 과정을 설명함으로써 시큐어 링킹이 실제로 사용되는 링크 시스템을 나타낼 수 있을 만큼 풍부한 표현력과 실용성을 가지고 있음을 증명한다. 또한 이 과정에서 나타난 어셈블리 코드 서명의 문제점에 대한 논의를 통해서 논리에 기반을 둔 링크 프레임워크가 가지는 장점을 보이고자 한다.

Abstract

When building a software system out of software components, the composition is not simple because of the complexity caused by diverse versions, digital signatures, static type information, and off-the-shelf components from various vendors. Well-established linking policies are one of the best solutions to solve the complexity problem at linking time. Secure Linking (SL) enables users to specify their linking policies which can be enforced at link time. Secure Linking framework is a framework based on a higher-order logic in order to help build a SL system. This paper shows that the Secure Linking logic is expressive enough to describe a real-world component composition system, the linking protocol of.NET. The paper also demonstrates the advantage of the logic-based linking framework by discussing the weakness of the code signing protocol in.NET which was found while we encoded the assembly linking system of.NET.

주제어

#component composition   #logical framework   #code security  

저자의 다른 논문

참고문헌 (17)

1. A. W. Appel and A. P. Felty. Dependent types ensure partial correctness of theorem provers. Journal of Functional Programming, 14(1):3-19, January 2004 
2. L. Bauer, A. W. Appel, and E. W. Felten. Mechanisms for secure modular programming in java. Technical Report CS-TR-603-99, Department of Computer Science, Princeton University, July 1999 
3. M. Blume and A. W. Appel. Hierarchical modularity. ACM Transactions on Programming Languages and Systems, 21:812-846, 1999 
4. A. Reid, M. Flatt, L. Stoller, J. Lepreau, and E. Eide. Knit: Component composition for systems software. In Proceedings of the Usenix Conference on Operating System Design and Implementation, pages 347-360, 2000 
5. M. Abadi, M. Burrows, B. Lampson, and G. Plotkin. A calculus for access control in distributed systems. ACM Transactions on Programming Languages and Systems, 15(4):706-734, September 1993 
6. Microsoft. Inside the .NET framework. http://msdn.microsoft.com/library/ 
7. D. Dean. The security of static typing with dynamic linking. In Proceedings of the Fourth ACM Conference on Computer and Communications Security, Zurich, Switzerland, 1997 
8. D. S. Platt. Introducing Microsoft .NET. Microsoft Press, 2001 
9. E. Wobber, M. Abadi, M. Burrows, and B. Lampson. Authentication in the Taosoperating system. ACM Transactions on Computer Systems, 12(1):3-32, 1994 
10. L. Bauer, M. A. Schneider, and E. W. Felten. A general and flexible access- control system for the web. In Proceedings of the 11th USENIX Security Symposium, August 2002 
11. L. Cardelli. Program fragments, linking, and modularization. In Proceedings of ACM Symposium on Principles of Programming Languages, pages 266277. ACM Press, January 1997 
12. P. T. Devanbu, P. W.-L. Fong, and S. G. Stubblebine. Techniques for trusted software engineering. In Proceedings of the 1998 International Conference on Software Engineering, pages 126-135, Los Alamitos, California, 1998 
13. G. Necula. Proof-carrying code. In Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL '97), January 1997 
14. A. W. Appel and E. W. Felten. Proof- carrying authentication. In 6th ACM Conference on Computer and Communications Security, November 1999 
15. F. Pfenning and C.Schurmann. System description: Twelf - a meta-logical framework for deductive systems. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202-206, July 1999 
16. E. Lee and A. W. Appel. Secure Linking: a Logical Framework for Policy- Enforced Component Composition (Extended Abstract). ACM SIGSOFT Symposium on the Foundations of Software Engineering, September, 2003 
17. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40:143-184, January 1993 

이 논문을 인용한 문헌 (0)

1. 이 논문을 인용한 문헌 없음