Tóm tắt - Bài báo này đề xuất một phương pháp để mô hình hóa và kiểm chứng biểu đồ trình tự UML 2.0 sử dụng SPIN/ PROMELA. Ý tưởng chính của phương pháp là xây dựng các mô hình mô tả hành vi của từng đối tượng trong biểu đồ trình tự UML 2.0. Các mô hình này biểu diễn dưới dạng các ôtômát vào/ra nhằm giữ nguyên tính tương tác giữa các đối tượng. Nghiên cứu đưa ra một kỹ thuật hỗ trợ chuyển đổi các mô hình này thành các đặc tả PROMELA để cung cấp cho bộ công cụ SPIN nhằm kiểm chứng tính đúng đắn của các biểu đồ tuần tự. Bằng cách đảm bảo tính chính xác của thiết kế phần mềm, một số thuộc tính có thể được đảm bảo như an toàn, ổn định và thực tế là không còn lỗ hổng nào. Một công cụ hỗ trợ cho phương pháp đề xuất cũng được cài đặt và thực nghiệm với một số hệ thống điển hình nhằm minh chứng cho tính đúng đắn, hiệu quả và dễ sử dụng. Cách tiếp cận này hứa hẹn sẽ được áp dụng trong thực tế.
REFERENCES[1]. ALAWNEH, L., DEBBABI, M., HASSAINE, F., JARRAYA, Y., & SOEANU, A., “A unified approach for verification and validation of systems and software engineering models”, In 13th Annual IEEE International Symposium and Workshop on Engineering of Computer-Based Systems (ECBS'06), pp. 409-418, 2006. [2]. BAIER, C., KATOEN, J. P., LARSEN, K. G., “Principles of model checking”, MIT Press, 2008. [3]. CLARKE, E. M., GRUMBERG, O., PELED, D., “Model checking”. MIT press, 1999. [4]. COBLEIGH, J. M., GIANNAKOPOULOU, D., PĂSĂREANU, C. S., “Learning assumptions for compositional verification”, In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, pp. 331-346, 2003. [5]. GRØNMO, R., MØLLER-PEDERSEN, B., “From UML 2 Sequence Diagrams to State Machines by Graph Transformation”. Journal of Object Technology, 10(8), 1-22, 2011. [6]. GUELFI, N., MAMMAR, A., “A formal semantics of timed activity diagrams and its PROMELA translation”, In 12th Asia-Pacific Software Engineering Conference, 2005. [7]. H. M. DUONG, L. K. TRINH, P. N. HUNG, “An Assume-Guarantee Model Checker for Component-Based Systems”, In IEEE-RIVF, pp. 22-26, 2013. [8]. JUSSILA, T., DUBROVIN, J., JUNTTILA, T., LATVALA, T., PORRES, I., & LINZ, J. K. U., “Model checking dynamic and hierarchical UML state machines”, Proc. MoDeV2a: Model Development, Validation and Verification, pp. 94-110, 2006. [9]. KNAPP, A., WUTTKE, J., “Model checking of UML 2.0 interactions”, In International Conference on Model Driven Engineering Languages and Systems, pp. 42-51, 2006. [10]. L. C. LUAN, P. N. HUNG, “A method for model generation from UML 2.0 sequence diagrams”, Proc. FAIR’9, Can Tho, pp. 619-625, 2016. [11]. LATELLA, D., MAJZIK, I., & MASSINK, M., “Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker”, Formal aspects of computing, 11(6), pp. 637-664, 1999. [12]. LIMA, V., TALHI, C., MOUHEB, D., DEBBABI, M., WANG, L., POURZANDI, M., “Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages”, Electronic Notes in Theoretical Com. Science, 254, pp.143-160, 2009. [13]. MIKK, E., LAKHNECH, Y., SIEGEL, M., & HOLZMANN, G. J. (1998). “Implementing statecharts in PROMELA/SPIN”, In Industrial Strength Formal Specification Techniques, Proc. 2nd IEEE Workshop, pp. 90-101, 1998. [14]. P. N. HUNG, T. KATAYAMA, “Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software”, In the 15th Asia-Pacific Software Engineering Conference, IEEE Computer Society Press, pp. 479-486, 2008. [15]. SCHÄFER, T., KNAPP, A., MERZ, S., “Model checking UML state machines and collaborations”, Electronic Notes in Theoretical Com. Sci., 55(3), pp.357-369, 2001. [16]. SIVERONI, I., ZISMAN, A., SPANOUDAKIS, G., “Property specification and static verification of UML models”, In Availability, Reliability and Security, pp. 96-103, 2008. [17]. VAN AMSTEL, M. F., LANGE, C. F., & CHAUDRON, M. R., “Four automated approaches to analyze the quality of UML sequence diagrams”. In Computer Software and Applications Conf., pp. 415-424, 2007. [18]. ZHANG, C. & DUAN, Z., “Specification and Verification of UML 2.0 Sequence Diagrams Using Event Deterministic Finite Automata”, in 'SSIRI (Companion)', IEEE Computer Society, pp. 41-46, 2011. [19]. OMG Unified Modeling Language. [Online]. http://www.omg.org/spec/UML/2.5/PDF. [20]. HOLZMANN, GERARD J (1997). "The model checker SPIN." IEEE Transactions on software engineering 23.5: 279. [21]. Basic SPIN Manual. [Online]. Available: http://spinroot.com/spin/Man/Manual.html |
Thông tin trích dẫn: PhD. Chi Luan Le, “A Method for Modeling and Verifying of UML 2.0 Sequence Diagrams using SPIN”, Nghiên cứu khoa học và công nghệ trong lĩnh vực An toàn thông tin, Tạp chí An toàn thông tin, Vol. 09, pp. 20-28, No. 01, 2019.
PhD. Chi Luan Le
22:00 | 22/02/2020
14:00 | 09/06/2020
09:00 | 28/05/2020
22:00 | 22/02/2020
17:00 | 27/05/2019
09:00 | 28/04/2024
Không chỉ tác động đến lĩnh vực an toàn thông tin, Bug Bounty còn được cho là cổ vũ cho nền kinh tế Gig Economy kiểu Orwell. Điều này có là một góc nhìn tiêu cực cho hình thức bảo mật này?
09:00 | 01/04/2024
Trong thời đại số ngày nay, việc quản lý truy cập và chia sẻ thông tin cá nhân trên các thiết bị di động thông minh đã trở thành vấn đề đáng quan tâm đối với mọi người dùng. Việc không kiểm soát quyền truy cập và sự phổ biến của dữ liệu cá nhân có thể gây ra các rủi ro về quyền riêng tư và lạm dụng thông tin. Bài viết này sẽ giới thiệu đến độc giả về Safety Check - một tính năng mới trên iOS 16 cho phép người dùng quản lý, kiểm tra và cập nhật các quyền và thông tin được chia sẻ với người và ứng dụng khác ngay trên điện thoại của chính mình, giúp đảm bảo an toàn và bảo mật khi sử dụng ứng dụng và truy cập dữ liệu cá nhân.
09:00 | 10/01/2024
Ngày nay, công nghệ trí tuệ nhân tạo (AI) có vai trò hết sức quan trọng trong mọi lĩnh vực của đời sống. Trong đó, lĩnh vực an toàn thông tin, giám sát an ninh thông minh có tiềm năng ứng dụng rất lớn. Bên cạnh các giải pháp như phát hiện mạng Botnet [1], phát hiện tấn công trinh sát mạng [2], việc ứng dụng AI trong giám sát an ninh, hỗ trợ điều tra tội phạm cũng đang được nghiên cứu, phát triển và ứng dụng rộng rãi. Trong bài báo này, nhóm tác giả đề xuất giải pháp sử dụng mô hình mạng nơ-ron tinh gọn phân loại tương tác giữa 2 người trong chuỗi ảnh rời rạc. Kết quả nghiên cứu có vai trò quan trọng làm cơ sở xây dựng và phát triển các mô hình phân loại hành động bất thường, phát hiện xâm nhập.
09:00 | 05/06/2023
Tấn công tiêm lỗi (Fault Injection Attack - FIA) là loại tấn công chủ động, giúp tin tặc xâm nhập vào các thiết bị điện tử, mạch tích hợp cũng như các thiết bị mật mã nhằm thu được khóa bí mật và đánh cắp thông tin. Tiêm lỗi có thể được thực hiện trong cả phần cứng và phần mềm. Bài báo này nhóm tác giả sẽ trình bày về các kỹ thuật, công cụ được thực hiện trong FIA.
08:00 | 11/01/2024 | Chính sách - Chiến lược
09:00 | 10/01/2024 | Giải pháp khác
09:00 | 05/01/2024|Chính sách - Chiến lược
09:00 | 05/01/2024|An ninh – Quốc Phòng
Có một số phương pháp để xác định mức độ an toàn của các hệ mật sử dụng độ dài khóa mã (key length) tham chiếu làm thông số để đo độ mật trong cả hệ mật đối xứng và bất đối xứng. Trong bài báo này, nhóm tác giả tổng hợp một số phương pháp xác định độ an toàn của hệ mật khóa công khai RSA, dựa trên cơ sở các thuật toán thực thi phân tích thừa số của số nguyên modulo N liên quan đến sức mạnh tính toán (mật độ tích hợp Transistor theo luật Moore và năng lực tính toán lượng tử) cần thiết để phá vỡ một bản mã (các số nguyên lớn) được mã hóa bởi khóa riêng có độ dài bit cho trước. Mối quan hệ này giúp ước lượng độ an toàn của hệ mật RSA theo độ dài khóa mã trước các viễn cảnh tấn công khác nhau.
08:00 | 04/04/2024
Mới đây, Cơ quan An ninh mạng và Cơ sở hạ tầng Hoa Kỳ (CISA) đã phát hành phiên bản mới của hệ thống Malware Next-Gen có khả năng tự động phân tích các tệp độc hại tiềm ẩn, địa chỉ URL đáng ngờ và truy tìm mối đe dọa an ninh mạng. Phiên bản mới này cho phép người dùng gửi các mẫu phần mềm độc hại để CISA phân tích.
13:00 | 17/04/2024
