디지털 라이브러리[ 검색결과 ]
C와 유사한 언어에서 정수-포인터 변환 지원을 위한 메모리 모델 설계: 이중 비결정성을 사용하여
http://doi.org/10.5626/JOK.2024.51.7.643
시스템 프로그래밍에서 포인터는 매우 중요한 요소이며, 정수-포인터 변환(Integer-Pointer Casting)을 포함한 프로그램에 정형 검증을 적용하는 것은 중요한 과제이다. 정수-포인터 변환을 포함한 프로그램을 정형 검증하기 위해서는 정수-포인터 변환을 지원하는 수학적으로 정의된 메모리 모델과 검증 에 사용할 증명 방법이 필요하다. 우리는 Coq 증명 도구 안에서 정수-포인터 변환을 지원하는 메모리 모델을 정의했다. 이 모델은 끝에서 한 칸 벗어난 포인터(one-past-the-end pointer)를 포함한 정수-포인터 연산과 관련된 패턴을 제대로 지원한다. 또한 우리가 정의한 모델을 프로그램 검증에 사용할 수 있도록 시뮬레이션 기반 증명 방법론을 새로 정의하고 적합성(Adequacy)을 증명했다. 마지막으로 우리의 접근 방법 이 타당함을 확인하기 위해 검증된 C 컴파일러인 CompCert의 메모리 모델과 의미 구조를 우리가 정의한 것으로 변경한 후 시뮬레이션을 통해서 CompCert의 최적화 검증 증명 중 두 개를 업데이트했다. 우리는 이 메모리 모델이 컴파일러와 정수-포인터 연산을 포함하는 프로그램 검증에 적용되기를 기대하고 있다.
정책기반의 분산서비스거부공격 대응방안 연구
2009년 이후 정부 및 민간부문에서는 DDoS 방어체계 구축을 위해 수백억 원의 예산을 투입해 왔으며, 그 결과 많은 정부 및 민간분야에 DDoS 대응을 위한 전용장비가 설치되었다. 그러나 이러한 기관 역시 DDoS 공격 발생 시 성공적인 방어가 이루어지지 않는 경우가 많은데, 이는 DDoS 대응 장비가 특정 공격 행위에만 대응할 수 있는 시그니처 중심의 방어 구조를 따르고 있기 때문이다. 이에 비해 방어자원 관점의 정책적 대응방법을 통할 경우, 공격 기법과 상관없이 서비스 자원의 가용성 확인을 통하여 시스템 이상여부 및 공격 유형의 종류를 확인할 수 있으며, 공격에 대한 대응 정책 또한 손쉽게 도출할 수 있다. 본 고에서는 기존의 공격 행위 중심의 방어체계에서 벗어나 방어자 관점의 DDoS 탐지 기법을 소개하고, 이를 통해 정책기반 서비스거부공격 대응방안을 제시한다.
사용자 맞춤형 분석 기반의 Hybrid 메시지 전송 기법
2009년을 기점으로, 스마트 기기 시장은 폭발적으로 성장하기 시작했다. 이렇게 보급된 스마트기기는 사용자에게 다양한 서비스를 제공한다. 그 중, 클라우드 메시징 서비스는 다양한 서비스에 적용되어 사용되고 있다. 클라우드 메시징 서비스는 비동기적으로 메시지를 전달하는 서비스를 의미한다. 클라우드 메시징 서비스를 통해 메시지를 모바일 단말에 전송하는 방식으로는 IP 기반 메시지 전송 기법과 Publish/Subscribe 기법이 있다. 각각의 기법은 메시지 전송을 위해 기본적으로 전송되어야 하는 메시지가 존재한다. 본 논문에서는 기본적으로 전송되어야 하는 메시지 량을 줄이기 위해, 사용자 맞춤형 기반 Hybrid 메시지 전송 기법을 제안한다. Hybrid 메시지 전송 기법에서는 Exponential Moving Average (EMA)와 K-means 알고리즘을 이용해 사용자 맞춤형 분석을 수행하고, 이를 이용해 각 시간대 별로 메시지 전송 기법을 결정하게 된다.
