Digital Library[ Search Result ]
Memory Model Design for Integer-Pointer Casting Support in C-like languages Via Dual Non-determinism
http://doi.org/10.5626/JOK.2024.51.7.643
In system programming, pointers are essential elements. However, applying formal verification methods to programs involving integer-pointer casting poses an important challenge. To address this challenge, a mathematically defined memory model that supports integer-pointer casting, along with proof techniques for verification, is necessary. This study presents a memory model that supports integer-pointer casting within the Coq proof assistant. The model accommodates patterns associated with integer-pointer operations, including one-past-the-end pointers. Additionally, a simulation-based proof technique is introduced, which enables the utilization of the model for program verification. The adequacy of this technique is established through proof. To validate the effectiveness of the approach, the defined memory model is integrated into CompCert, a verified C compiler, replacing its original memory model. Subsequently, two proofs of CompCert's optimization verification are updated using the simulation technique. It is anticipated that the proposed memory model will find applications in program and compiler verification tasks involving integer-pointer operations.
Policy Based DDoS Attack Mitigation Methodology
Hyuk Joon Kim, Dong Hwan Lee, Dong Hwa Kim, Myung Kil Ahn, Yong Hyun Kim
Since the Denial of Service Attack against multiple targets in the Korean network in private and public sectors in 2009, Korea has spent a great amount of its budget to build strong Internet infrastructure against DDoS attacks. As a result of the investments, many major governments and corporations installed dedicated DDoS defense systems. However, even organizations equipped with the product based defense system often showed incompetency in dealing with DDoS attacks with little variations from known attack types. In contrast, by following a capacity centric DDoS detection method, defense personnel can identify various types of DDoS attacks and abnormality of the system through checking availability of service resources, regardless of the types of specific attack techniques. Thus, the defense personnel can easily derive proper response methods according to the attacks. Deviating from the existing DDoS defense framework, this research study introduces a capacity centric DDoS detection methodology and provides methods to mitigate DDoS attacks by applying the methodology.
A Method for Hybrid Message Transmission based on User-Customized Analysis
Yong-Hyun Kim, Jae-Sic Bong, Eui-Nam Huh
From 2009, the market of smart devices has been rapidly increasing. These devices provide various services to users. The cloud messaging service, especially, is applied to many various services, and sends messages asynchronously. In the cloud messaging service, there are two methods for message transmission, message transmission based on an IP address and a publish/subscribe technique. Each technique uses basic messages in order to send messages to mobile devices. In this paper, the hybrid message transmission, based on user-customized analysis to reduce basic messages, is proposed. The hybrid message transmission uses Exponential Moving Average (EMA) and K-means algorithms for user-customized analysis, and determines the message transmission techniques in each timeslot.
Search
Journal of KIISE
- ISSN : 2383-630X(Print)
- ISSN : 2383-6296(Electronic)
- KCI Accredited Journal
Editorial Office
- Tel. +82-2-588-9240
- Fax. +82-2-521-1352
- E-mail. chwoo@kiise.or.kr