$\require{mediawiki-texvc}$

연합인증

연합인증 가입 기관의 연구자들은 소속기관의 인증정보(ID와 암호)를 이용해 다른 대학, 연구기관, 서비스 공급자의 다양한 온라인 자원과 연구 데이터를 이용할 수 있습니다.

이는 여행자가 자국에서 발행 받은 여권으로 세계 각국을 자유롭게 여행할 수 있는 것과 같습니다.

연합인증으로 이용이 가능한 서비스는 NTIS, DataON, Edison, Kafe, Webinar 등이 있습니다.

한번의 인증절차만으로 연합인증 가입 서비스에 추가 로그인 없이 이용이 가능합니다.

다만, 연합인증을 위해서는 최초 1회만 인증 절차가 필요합니다. (회원이 아닐 경우 회원 가입이 필요합니다.)

연합인증 절차는 다음과 같습니다.

최초이용시에는
ScienceON에 로그인 → 연합인증 서비스 접속 → 로그인 (본인 확인 또는 회원가입) → 서비스 이용

그 이후에는
ScienceON 로그인 → 연합인증 서비스 접속 → 서비스 이용

연합인증을 활용하시면 KISTI가 제공하는 다양한 서비스를 편리하게 이용하실 수 있습니다.

보안 정형 검증 도구를 이용한 보안 S/W 검증 방안

Verification Methodology of Security S/W using Security Formal Verification Tool

한국정보처리학회 2005년도 제23회 춘계학술발표대회, 2005 May 13, 2005년, pp.1091 - 1094  

김기환 (동의대학교 컴퓨터공학과) ,  장승주 (동의대학교 컴퓨터공학과) ,  박일환 (한국전자통신연구원 국가보안기술연구소)

초록
AI-Helper 아이콘AI-Helper

보안 소프트웨어 개발을 위한 정형 기법은 소프트웨어의 안정성과 신뢰성을 보장할 수 있는 기반을 마련해 준다. 정형화 기법에는 정형 명세와 정형 검증으로 분류할 수 있으며, 이를 위해 여러 도구가 제공되고 있다. 본 논문에서는 보안 소프트웨어 개발을 위한 RoZ 정형 명세 도구를 이용하여 ACS(Access Control System)의 UML 모델을 통한 Z 명세 자동 생성 과정을 살펴본다. 그리고, 정형 검증 도구인 Z/EVES를 이용하여 ACS 의 특정 기능의 명세에 대한 검증 과정을 수행함으로써, 소프트웨어 설계에 따른 보안 소프트웨어의 안정성을 보장할 수 있는 개발 방안을 제시하였다.

AI 본문요약
AI-Helper 아이콘 AI-Helper

* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.

문제 정의

  • 명세화된 시스템을 통하여 완전히 안정된 소프트웨어라고 보장할 수는 없다 이러한 이유 때문에 정형 검증 과정을 통하여 설계된 소프트웨어의 각 항목에 대한 검증 절차가 필요하다. 검증 절차를 수행하기 위해 사용되는 도구에는 여러 가지 있지만, 본 논문에서는 Z/EVES 보안 정형 검증 도구를 이용함으로써, 소프트웨어 설계에 따른 UML 모델을 통해 생성된 Z 명세의 각 오퍼레이션에 대한 전제 조건들을 검사함으로써 소프트웨어 설 계시 제시한 규제 조건을 만족할 수 있도록 보장한다
  • 본 논문에서는 UML과 정형 명세 언어인 Z와의 조합을 이용함으로써 명세를 더욱 더 향상 시킬 수 있는 방법을 제시하였다. 이를 이용하여 Z/EVES 정형 검증 도구를 통해 보안 소프트웨어의 안정성 및 신뢰성을 보장할 수 있는지에 대한 검증 절차를 수행하였다.
  • 본 논문에서는 접근 제어 시스템을 구현해 봄으로써 소프트웨어의 정형 명세 및 개발 방안을 제시하였다. 소프트웨어의 명세 과정은 Z 언어를 이용하여 ACS(Access Control System)에 대한 명세 과정을 수행하게 되는데 Z 언어를 사용하기 위해 제공하고 있는 도구가 RoZ이다.
  • 본 논문의 실험에서는 Z/EVES 정형 검증 도구를 이용하여 ACS(접근제어시스템)에 대한 검증 과정을 수행해 보았다. 정형화 기법을 이용한 보안 소스 코드 명세 및 검증 과정은 다음 세 가지 과정을 통하여 완료할 수 있다.
  • 본 절에서는 ACS의 UML 모델을 이용하여 Z 명세를 하는 과정에 대해 설명을 한 것이다. Rose 4.

가설 설정

  • [그림 2] Access Control System 구현을 위 한 UML 모델

    ① 모든 사람은 적어도 하나의 전화번호를 가지고 있다.

본문요약 정보가 도움이 되었나요?
섹션별 컨텐츠 바로가기

AI-Helper ※ AI-Helper는 오픈소스 모델을 사용합니다.

AI-Helper 아이콘
AI-Helper
안녕하세요, AI-Helper입니다. 좌측 "선택된 텍스트"에서 텍스트를 선택하여 요약, 번역, 용어설명을 실행하세요.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.

선택된 텍스트