Một phương pháp đặc tả logic cho việc đánh giá và phân tích lỗ hổng an ninh mạng

46 TRNG I HC TH  H NI 
M7T PH"#NG PH$P .CC T% LOGIC CHO VIC 
 .$NH GI$ V- PHDN TECH LF HNG AN NINH M>NG 
Trần Bá Hùng1, Nguyễn Đức Giang1, Bùi Thị Thư1, Lưu Thị Bích Hương2 
1Viện Công nghệ Thông tin, Viện Hàn lâm Khoa học và Công nghệ Việt Nam 
2Trường Đại học Sư phạm Hà Nội 2 
Tóm tắt: Điều quan trọng đối với các quản trị viên hệ thống là phải biết về những lỗ hổng 
bảo mật. Tuy nhiên, các phương pháp đánh giá tính dễ tổn thương hiện tại có thể gặp 
phải các vấn đề về tỷ lệ sai lệch cao, thời gian tính toán dài. Hơn nữa, chúng chỉ có khả 
năng định vị các lỗ hổng riêng lẻ trên một máy chủ lưu trữ mà không cần quan tâm đến 
hiệu quả tương ứng của các lỗ hổng trên máy chủ hoặc một phần của mạng với các lỗ 
hổng có thể được phân phối giữa các máy khác nhau. Để giải quyết những vấn đề 
này,chúng tôi đưa ra một phương pháp hình thức sử dụng đặc tả logic cho việc đánh giá 
và phân tích lỗ hổng an ninh mạng. Với phương pháp này các lỗ hổng được phát hiện mà 
không cần phải mô phỏng các cuộc tấn công và nó cũng có thể dễ dàng tích hợp với các 
công cụ bảo mật khác dựa trên cơ sở dữ liệu quan hệ. 
Từ khóa: An ninh mạng, đánh giá tính dễ tổn thương, lỗ hổng bảo mật, thuộc tính logic 
Nhận bài ngày 14.5.2017; gửi phản biện, chỉnh sửa và duyệt đăng ngày 10.9.2017 
Liên hệ tác giả: Trần Bá Hùng; Email: tbhung@ioit.ac.vn 
1. GIỚI THIỆU 
Ngày nay, với sự gia tăng mạnh mẽ của mạng máy tính và sự phức tạp của phần mềm 
máy tính, các lỗ hổng bảo mật cũng tăng nhanh ở các doanh nghiệp lớn [3]. Vì nhiều vấn 
đề về bảo mật gây ra bởi các lỗ hổng ẩn trong các mạng máy tính, điều cực kỳ quan trọng 
là các quản trị viên hệ thống phải biết về các lỗ hổng này. Phân tích những lỗ hổng này và 
tìm ra cách khai thác, khắc phục chúng là rất quan trọng cho các hệ thống thông tin của tổ 
chức, doanh nghiệp [9], có nhiều nghiên cứu để phát triển kỹ thuật đánh giá tính dễ tổn 
thương như xác định các lỗ hổng bảo mật hiện có trong mạng. Trong thực tế, cùng với 
tường lửa, hệ thống phát hiện xâm nhập, mã hóa và bảo vệ chống virus, đánh giá tổn 
thương là một trong những kỹ thuật cốt lõi trong việc bảo vệ chống lại các cuộc tấn công 
mạng. Các phương pháp phân tích lỗ hổng bảo mật được thực hiện tự động, chẳng hạn như 
Internet Security System (ISS) Internet Scanner, Nessus, andsoon [15]. Trong bài báo này 
TP CH KHOA HC − S
 18/2017 47 
chúng tôi sẽ giới thiệu một phương pháp mới để phân tích đánh giá lỗ hổng an ninh 
mạng đó là phương pháp hình thức sử dụng đặc tả logic để giải quyết bài toán lỗ hổng an 
ninh mạng. 
Để giải quyết vấn đề này bài báo trình bày một hệ thống đánh giá tính dễ bị tổn thương 
cho mô hình mạng NetScope dựa trên ngôn ngữ OVAL (Open Vulnerability Assessment 
Language), bao gồm ba module chính: kiểm tra phân chia các tác nhân (distributed 
inspection agents), phương pháp phân tích(analysis engine) và trung tâm dữ liệu(data 
center). Các lỗ hổng được xác định thông qua OVAL đồng thời kết hợp các lỗ hổng tương 
ứng với các cuộc tấn công trong một mạng thông qua lí thuyết logic vị từ. 
Trong các phần tiếp theo của bài báo chúng tôi trình bày phương pháp đặc tả logic cho 
việc đánh giá và phân tích lỗ hổng an ninh mạng. Phần ba của bài báo là kết quả thử 
nghiệm phương pháp hình thức sử dụng đặc tả. Cuối cùng là kết luận của bài báo. 
2. PHƯƠNG PHÁP ĐẶC TẢ LOGIC CHO VIỆC ĐÁNH GIÁ VÀ PHÂN 
TÍCH LỖ HỔNG AN NINH MẠNG 
2.1. Mô hình hệ thống lỗ hổng NetScope 
2.1.1. Một số khái niệm cơ bản 
Phương pháp phân tích của hệ thống NetScope được đề xuất trong bài báo này dựa 
trên lý thuyết logic vị từ đơn giản được phân chia thành hai phần: phần riêng biệt và vị từ. 
Các vị từ có các yếu tố cơ bản, trước tiên chúng ta giới thiệu các định nghĩa sau được sử 
dụng cho NetScope [7]. 
Định nghĩa 1. [19] Kiểu tấn công V: gồm ba thành phần (fact, prerequisite, 
consequence) để đại diện cho điều kiện tiên quyết và kết quả của mỗi kiểu tấn công. Mô tả 
của mỗi phần tử được liệt kê như sau: 
− Fact: là một tập hợp các cá thể, mỗi cá thể có miền liên kết các giá trị, được ký hiệu 
bởi {x1,..., xn}. 
− Prerequisite: Là điều kiện tiên quyết chỉ ra những cái gì cần phải đúng để thực hiện 
tấn công một cách thành công được thể hiện bằng công thức vị từ như sau: P1(x1) ... 
Pp(xp). 
− Consequence: Mô tả những gì có thể đúng nếu cuộc tấn công thực sự thành công, là 
một tập hợp các công thức cơ sở logic, tất cả các biến được biểu diễn bởi công thức 
{P1(x1)..., Pq (xq)}. 
48 TRNG I HC TH  H NI 
Định nghĩa 2. Một tấn công tức thời v: là tập hữu hạn của tập hợp trên fact của kiểu 
tấn công V, trong đó mỗi bộ được kết hợp với một giá trị xác định. 
Định nghĩa 3. [20] Kiểu lỗ hổng D:của bất kỳ thuộc tính hệ thống nào có thể được sử 
dụng như là một điều kiện tiên quyết của các kiểu tấn công, tức là mỗi công thức thuộc tính 
cơ sở là điều kiện tiên quyết cho các kiểu tấn công được biết đếntrong CVE (Common 
Vulnerabilities and Exposures), quyền đầy đủ của người dùng trên victim/attack host và 
các kịch bản tấn công để khởi động các cuộc tấn công. 
Định nghĩa 4. Lỗ hổng khởi tạo d: làmột lỗ hổng cụ thể với các địa chỉ IP xác định 
tương ứng với một kiểu dễ bị tấn công D. 
Định nghĩa 5. Quan hệ tấn công/lỗ hổng làcuộc tấn công tương ứng v tương quan với 
lỗ hổng được tạo ra d nếu có tồn tại pP(v) sao cho d bao hàm p, trong đó P(v) là tập hợp 
của tất cả các vị từ xuất hiện trong điều kiện tiên quyết và có đối số được thay thế bằng các 
giá trị thuộc tính tương ứng của một bộ trong d. 
2.1.2. Kiến trúc của hệ thống mô tả lỗ hổng NetScope 
Kiến trúc tổng thể của NetScope đề xuất trong bài báo này được thể hiện trong Hình 1. 
Nó bao gồm ba phần: tác nhân kiểm tra (inspection agents), trung tâm dữ liệu (data center) 
và công cụ phân tích (analysis engine). Các chức năng của từng phần được mô tả như sau: 
Hình 1. Kiến trúc của hệ thống mô tả lỗ hổng NetScope. 
− Inspection agent: Mỗi một inspection agentđược triển khai trên một m ... hiện đường dẫn tấn công dẫn đến một mục tiêu cụ thể được tìm thấy. 
Được chỉ định nếu giá trị của dấu hiệu là 1, có nghĩa là có một đường dẫn tấn công ít nhất. 
Nếu không, không tìm thấy đường tấn công. 
correlation(i, temp) là hàm các quy tắc tương quan để xác định liệu một cuộc tấn công 
instantiated có thể thành công, cho dù các giá trị tương ứng với cùng một ký tự 
"ATTACK", "Mid_Host" hay "VICTIM" trong mẫu kiểu bản ghi là hoàn toàn bình đẳng 
trong bản ghi instantiated i nếu có, cuộc tấn công này sẽ xảy ra, và giá trị trả về tương quan 
chức năng là TRUE. Nếu không, sẽ không có cuộc tấn công xảy ra và giá trị trả về là 
TP CH KHOA HC − S
 18/2017 57 
FALSE. Ví dụ một kiểu tấn công cụ thể IIS_RDS, giả sử một loại bản ghi và một bản ghi 
khởi tạo i = {Money, NULL, Money, Maude, Maude, NULL}, một cuộc tấn công kiểu tấn 
công khởi tạo IIS_RDS thành công vì các giá trị tương ứng với ATTACK và VICTIM 
trong temp là Money và Maude trong i. 
Output(i,temp) là hàm mà các cá nhân thay thế của một kiểu tấn công cụ thể 
(ATTACK, Mid_Host, VICTIM)với các giá trị tương ứng trong i, tương ứng với ba chuỗi: 
ATTACK, Mid_Host hoặc VICTIM hoặc trong temp. Ví dụ được liệt kê trong tương quan 
về chức năng (i, temp), cuộc tấn công khởi tạo IIS_RSD (Money, Maude) được tạo ra thông 
qua chức năng IIS_RDS (output (i, temp)). 
Ins (P(et))∩////σ/Π/ là hàm khởi tạo của mỗi công thức vị từ P(et) theo tập các thông 
tin ban đầu. Các hành động của intersection/union/difference/selection/projection/joinđược 
xác định trong cơ sở dữ liệu quan hệ. 
Hình 5. Thuật toán tương quan attack/vulnerability. 
Hình 5 trình bày các thuật toán được đề xuất về mối tương quan attack/vulnerability. 
Nó bao gồm hai thủ tục: Forward_search và Backward_search. Đối với giới hạn không 
gian và các chi tiết của Backward_search tương tự như của Forward_search, chỉ có chi tiết 
của Forward_search được mô tả trong thuật toán tương quan attack/vulnerability. Thủ tục 
58 TRNG I HC TH  H NI 
Forward_search bắt đầu kết hợpcác điều kiện tiên quyết của các kiểu tấn công với các lỗ 
hổng gốc ban đầu, trong khi giai đoạn ban đầu của thủ tục Backward_search là kết hợp các 
hậu quả của các kiểu tấn công với mục tiêu được bảo vệ. Hai thủ tục này đảm bảo rằng các 
cuộc tấn công cần thiết và đầy đủ đối với các điều kiện ban đầu và mục tiêu được tìm thấy. 
Hơn nữa, phương pháp chỉ phân tích các loại tấn công mà điều kiện tiên quyết của nó được 
thay đổi và phù hợp với chúng với tính dễ bị tổn thương được áp dụng mỗi lần lặp. 
Phương pháp này có thể tiết kiệm rất nhiều thời gian và không gian trong toàn bộ quá trình 
tương quan. 
Module 4: Đường dẫn tấn công 
Trong mô hình phân tích lỗ hổng mạng, modulehiển thị phân tích bảng kết quả tương 
quan, và tiếp tục xây dựng một sơ đồ trực tiếp các điều kiện prerequisites/consequences 
phụ thuộc vào các cuộc tấn công và các lỗ hổng với các chức năng của RDBMS [14]. 
Thuật toán trực quan hóa các đường dẫn tấn công được thể hiện trong Hình 6. Một phương 
pháp biểu diễn linh hoạt có cả lỗ hổng và tấn công như là đỉnh được sử dụng để diễn tả các 
đường dẫn tấn công tiềm ẩn. Các cạnh trực tiếp chỉ đại diện cho sự phụ thuộc chung. Một 
cạnh phụ thuộc e = (v, s) đi từ lỗ hổng v đến tấn công s có nghĩa là v là điều kiện tiên quyết 
của s. Tương tự, biên độ phụ thuộc e = (v, s) đi từ tấn công đến lỗ hổng v có nghĩa là v là 
hệ quả của s. Đồng thời, chúng tôi chỉ hiển thị một loại lỗ hổng, tức là chỉ như các điều 
kiện tiên quyết của cuộc tấn công trong đồ thị trực tiếp để giảm không gian hiển thị. Kết 
quả là một tập hợp các đường dẫn tấn công trực quan dẫn từ trạng thái mạng ban đầu đến 
một mục tiêu tấn công được xác định trước. Nó cũng hiển thị như thế nào kẻ tấn công sẽ 
khai thác lỗ hổng hệ thống để đạt được bước xâm nhập của mình từng bước. Công việc này 
giúp các quản trị viên phát hiện các chiến thuật tấn công cấp cao. 
Hình 6. Thuật toán trực quan hóa các đường dẫn tấn công. 
TP CH KHOA HC − S
 18/2017 59 
2.3. Các kỹ thuật thực hiện chính của hệ thống NetScope 
Thiết kế của NetScope phải đáp ứng các yêu cầu về truyền thông thời gian thực và bảo 
mật dữ liệu. Hai loại cơ chế được áp dụng với việc xem xét truyền thông an toàn và hiệu 
suất thời gian quan trọng. 
2.3.1. Giao tiếp an toàn qua SSL / TLS 
Bất kỳ phần mềm ứng dụng nào với kiến trúc C/S phải giải quyết vấn đề giao tiếp an 
toàn giữa máy chủ và máy khách. Có hai loại yêu cầu truyền thông trong hệ thống 
NetScope: 
− Truyền dữ liệu giữa tác nhân kiểm tra và trung tâm dữ liệu, giữa công cụ phân tích 
và trung tâm dữ liệu. Cơ chế mã hoá dữ liệu được cung cấp bởi RDBMS SQL Server 2000 
được thông qua để đảm bảo tính bảo mật của việc vận chuyển tập dữ liệu. 
− Kiểm soát truyền thông tin giữa công cụ phân tích và tác nhân kiểm tra. Giao thức 
vận chuyển SSL/TLS giữa lớp vận chuyển và lớp ứng dụng được giới thiệu để đạt được mã 
hóa tin nhắn giữa công cụ phân tích và tác nhân kiểm tra. Một quá trình giao tiếp hoàn 
chỉnh giữa chúng được thể hiện trong Hình 7. Nó được chia thành 5 cụm thông tin liên lạc: 
Thông tin xin chào, yêu cầu thu thập dữ liệu, trả lời về thu thập dữ liệu, thông báo kết thúc 
thu thập dữ liệu và thông tin kết thúc phiên làm việc. Trong một quá trình đánh giá hoàn 
chỉnh, năm cụm từ này xảy ra theo một trật tự cố định. 
Hình 7. Giao tiếp giữa công cụ phân tích và tác nhân kiểm tra. 
2.3.2. Kỹ thuật để cải thiện hiệu suất thời gian 
Có hai kỹ thuật để cải thiện hiệu suất thời gian là đa luồng và chức năng lười biếng 
được áp dụng để cải thiện hiệu suất thời gian. 
− Đa luồng (Multi-thread): Một luồng công việc độc lập được khởi động cho mỗi công 
việc đánh giá trên công cụ phân tích. Hơn nữa, tất cả các luồng chạy song song từ đầu đến 
60 TRNG I HC TH  H NI 
cuối của đánh giá lỗ hổng. Ví dụ, công cụ phân tích sẽ khởi động tối đa 255 luồng cho toàn 
bộ phân lớp mạng C. Cơ chế đa luồng có thể cải thiện hiệu quả đánh giá trong một mạng 
lưới quy mô lớn, bởi vì một chủ đề khác vẫn thực hiện nhiệm vụ đánh giá khi một chủ đề 
đang đợi chuyển dữ liệu vào trung tâm dữ liệu. 
− Hàm lười (Lazy function): Một tùy chọn chức năng lười biếng được đặt trên tác 
nhân kiểm tra để giảm thời gian chạy. Nó có nghĩa là nếu chúng ta kích hoạt tùy chọn này 
trên một tác nhân cụ thể, nó không khởi động một chủ đề khi nhận được yêu cầu thu thập 
dữ liệu ngay lập tức. Ngược lại, nó xác định xem có tồn tại một luồng công việc trong hệ 
thống không. Nếu có, nó chờ đợi cho kết thúc của chủ đề làm việc và nộp kết quả của nó 
cho công cụ phân tích. Nếu không, nó bắt đầu một chủ đề mới cho nhiệm vụ này. Khi một 
tác nhân nhận được nhiều yêu cầu cùng một lúc, nó thực sự khởi động một luồng để tiết 
kiệm được nhiều tài nguyên hệ thống. 
3. THỬ NGHIỆM 
Môi trường thí nghiệm thể hiện trong Hình 8 được thiết lập để kiểm tra hiệu năng của 
hệ thống NetScope trong việc đánh giá chính xác, hiệu quả và xây dựng các đường tấn 
công tiềm ẩn. Công cụ phân tích của hệ thống NetScope đã được thiết lập trên máy chủ 
192.168.7.12 để thiết lập các tùy chọn đánh giá, thực hiện hệ thống điều khiển và phân tích 
các kết quả được lưu trữ trong trung tâm dữ liệu. 
Hình 8. Mô hình thử nghiệm. 
Ta xem xét các máy chủ khác trong mạng này như các mục tiêu đánh giá và thiết lập 
các tác nhân kiểm tra trên các máy này để thu thập tập dữ liệu về cấu hình hệ thống. 
TP CH KHOA HC − S
 18/2017 61 
Thí nghiệm 1: Trên Mail sever với hai nhóm 
Nhóm 1: Đánh giá an toàn đối với IE 6.0 trên máy chủ mail chạy Win2K mà không có 
bản vá bởi hai hệ thống: NetScope và MBSA. Kết quả được trình bày trong Bảng 4. 
Nhóm 2: Cấu hình của mail server được thay đổi bằng cách cài đặt SP1 của IE 6.0 và 
IIS 5.0, và hai hệ thống đánh giá được sử dụng để tìm các lỗ hổng của IIS 5.0. Bảng 5 liệt 
kê các kết quả bằng cách áp dụng MBSA và NetScope. 
Bảng 4. Kết quả kiểm tra IE 6.0 trong nhóm 1 của thí nghiệm 1 
Bảng 5. Kết quả kiểm tra IE 6.0 trong nhóm 1 của thí nghiệm 1 
Kết quả đánh giá IIS 5.0 trong nhóm 2 của thí nghiệm 1 
Thí nghiệm 2: Kiểm tra cho nhiều máy chủ 
Kết quả thời gian tính toán trung bình cho nhiều máy chủ với 343 định nghĩa về lỗ 
hổng được thể hiện trong Hình 9. 
Hình 9. Thời gian tính toán trung bình cho nhiều máy chủ của NetScope. 
62 TRNG I HC TH  H NI 
4. KẾT LUẬN 
Trong bài báo này chúng tôi đã trình bày phương pháp mới đó là phương pháp hình 
thức đặc tả logic cho việc đánh giá và phân tích lỗ hổng an ninh mạng, các kết quả đã được 
trình bày ở nội dung bài báo này cho thấy lợi ích của việc sử dụng phương pháp hình thức 
trong việc áp dụng vào vấn đề an toàn an ninh mạng đang là vấn đề thời sự nóng hiện nay 
ở Việt Nam cũng như trên toàn thế giới. Trong thời gian tới hướng tiếp theo từ kết quả của 
bài báo này chúng tôi sẽ trình bày phương pháp xây dựng đồ thị tấn công khi đã đánh giá 
và phân tích lỗ hổng an ninh thông qua đó giúp các nhà quản trị hay người dùng có thể 
nhận biết và phán đoán các cuộc tấn công mạng thông qua lỗ hổng hệ thống mạng. 
Cuối cùng nhóm tác giả cũng xin chân thành cảm ơn đề tài CS17.11“Phương pháp 
hình thức dựa trên đặc tả logic cho việc phát hiện và phân tích lỗ hổng an ninh mạng” đã 
hỗ trợ để tác giả có thể hoàn thành bài báo này. 
TÀI LIỆU THAM KHẢO 
1. Ammann, P., Wijesekera, D., & Kaushik, S. (2002), “Scalable, graphbased network 
vulnerability analysis”.Proceedings of 9th ACMConference on Computer and Communication 
Security, Washington, D.C., USA 
2. Baldwin, R. (1994), Kuang.“Rule based security checking. Cambridge”:MIT Technical 
Report, MIT Lab for Computer Science,Programming Systems Research Group. 
3. CERT Coordination Center (2006), CERT/CC statistics 1988–2004.Pittsburgh: CERT 
Coordination Center accessed September 24, from  
4. Deraison, R., Gula, R., & Hayton, T. (2005), Passive vulnerabilityscanning: Introduction to 
NeVO. Accessed June 10. 
5. Farmer, D., & Spafford, E. H. (1991), “The cops security checkersystem”. West Lafayette: 
Purdue University Technical report,CSD-TR-993. 
6. Fithen, W. L., Hernan, S. V., O’Rourke, P. F., et al. (2004), Formalmodeling of 
vulnerabilities. Bell Labs Technical Journal, 8(4), pp.173–186. 
7. Geng, S., Qu, W., & Zhang, L. (2001), Discrete mathematics pp. 34-56. Beijing: Tsinghua 
University Press. 
8. Help and Support Home, Microsoft (2004), Microsoft baseline securityanalyzer (MBSA) 
version 1.2.1 is available. Accessed October 6. 
TP CH KHOA HC − S
 18/2017 63 
9. Hsu, C., & Wallace, W. (2007). “An industrial network flowinformation integration model for 
supply chain management and intelligent transportation”. Enterprise Information Systems, (1-
3), pp.327–351. 
10. International Institute of Standards and Technology (2004), ICATmetabase-your CVE 
vulnerability search engine. Accessed June10. 
11. Internet Security Systems (2005), Vulnerability assessment. AccessedMarch 10, 2005, from 
12. Jajodia, S., Noel, S., & O’Berry, B. (2003), Topological analysis ofnetwork attack 
vulnerability. Managing cyber threats: Issues, approaches and challenges, chapter 5. Norwell: 
Kluwer Academic. 
13. Kotenko, I. (2003), “Active vulnerability assessment of computernetworks by simulation of 
complex remote attacks”. InternationalConference on Computer Networks and Mobile 
Computing, October 20–23, Shanghai, China, pp.40–47, 
14. Li, T., Feng, S., & Li, L. (2001), Information visualization forintelligent decision support 
systems. Knowledge-Based Systems,14(5–6), pp.259–262. 
15. Martin, R. A. (2003), “Integrating your information security vulnerability management 
capabilities through industry standards (CVE& OVAL)”. IEEE International Conference on 
Systems, Man andCybernetics, 2,, October 5–8, pp.1528–1533 
16. McAfee (2003),  
17. Ritchey, R., & Ammann, P. (2000), “Using model checking to analyzenetwork 
vulnerabilities”, Proceedings of IEEE Symposium onSecurity and Privacy, Oakland: IEEE. pp. 
156–165. 
18. Zerkle, D., & Levitt, K. (1996), Netkuang—a multi-host configurationvulnerability checker, 
Proceedings of the 6th USENIX SecuritySymposium, San Jose, California, USA. 
19. Ning, P., & Cui, Y. (2002), “An intrusion alert correlator based on prerequisites of intrusions”. 
Raleigh: North Carolina State University Technical Report, TR-2002-01, Department of 
Computer Science. 
20. Ritchey, R., Berry, B., & Noel, S. (2002), “Representing TCP/IP connectivity for topological 
analysis of network security”, The 18th Annual Computer Security Applications Conference, 
December 9–13,San Diego, CA, USA. 
21. Wojcik, M., Bergeron, T., Wittbold, T., et al. (2005), “Introduction to OVAL: A new language 
to determine the presence of software vulnerabilities”, Accessed July 10, 2005. 
 intro.html. 
22. ICAT (2004), The ICAT Metabase, National Institute of Standards and Technology, Computer 
Security Division, Gaithersburg, MD,  
64 TRNG I HC TH  H NI 
USING A LOGICAL SPECIFICATION METHOD FOR 
EVALUATING AND ANALYZING NETWORK SECURITY 
VULNERABILITIES 
Abstract: It is important for system administrators to know about security vulnerabilities. 
However, existing vulnerability assessment methods may experience high bias rates, long 
calculation times. Moreover, they are only capable of locating individual vulnerabilities 
on a host server regardless of the corresponding performance of vulnerabilities on the 
server or part of the network with vulnerabilities that can be addressed. Distributed 
among different machines. To address these issues, we propose a formal methodology 
that uses a logical specification for evaluating and analyzing network security 
vulnerabilities. With this method vulnerabilities are detected without the need to simulate 
attacks and it can also easily integrate with other security tools based on relational 
databases. 
Keywords: Network security, vulnerability assessment, Security vulnerability, Predicate 
logic