Luận Văn Thạc Sĩ Về Kiểm Tra Ứng Dụng Android Sử Dụng Mô Hình

Đề tài Kiểm Tra Ứng Dụng Android Bằng Mô Hình Trong Luận Văn ... với cơ sở khoa học chặt chẽ, đóng góp giá trị cho nghiên cứu và thực tiễn chuyên

• Tác giả: Nguyen Thanh Hong
• Người hướng dẫn: PGS. Quan Thanh Tho
• Trường học: Đại Học Quốc Gia TP. HCM
• Chuyên ngành: Khoa Học Máy Tính
• Đề tài: Kiểm Tra Ứng Dụng Trên Điện Thoại Di Động Android Bằng Kiểm Tra Mô Hình
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2013
• Địa điểm: TP. HCM

Mục lục chi tiết

• NHIỆM VỤ LUẬN VĂN THẠC SĨ
• TÓM TẮT LUẬN VĂN
• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: PHÁT BIỂU VẤN ĐỀ
• 1.1. Những vấn đề về bảo mật của điện thoại Android
• 1.2. Các phương pháp giải hiện tại
• 1.3. Mục tiêu của luận văn
• 1.4. Đóng góp của luận văn
• 1.5. Cấu trúc luận văn
• 2. CHƯƠNG 2: NHỮNG CƠ SỞ LÝ THUYẾT NỀN TẢNG
• 2.1. Tổng quan về Android
• 2.1.1. Cấu trúc hệ điều hành Android
• 2.2. Android Security Framework
• 2.2.1. Application Sandbox
• 2.2.2. Permission
• 2.3. Sơ lược về một ứng dụng trên Android
• 3. CHƯƠNG 3: TỔNG THUẬT CÁC CÔNG TRÌNH LIÊN QUAN
• 3.1. Các hướng nghiên cứu hiện nay
• 3.2. Thảo luận về các hướng nghiên cứu
• 4. CHƯƠNG 4: PHƯƠNG PHÁP GIẢI QUYẾT VẤN ĐỀ VÀ HỆ THỐNG ỨNG DỤNG
• 4.1. Giải quyết vấn đề
• 4.2. Framework tổng quát
• 4.3. Đặc tả thành phần Android Model Checker
• 4.4. Đặc tả phần chương trình trừu tượng
• 4.5. Đặc tả phần assertions
• 4.6. Cách thức xử lí kiểm tra mô hình
• 5. CHƯƠNG 5: THỰC NGHIỆM
• 5.1. Thực nghiệm 1: kiểm tra lỗi bảo mật của ứng dụng Android
• 5.1.1. Phát hiện lỗi rò rỉ tường minh (explicit leak)
• 5.1.2. Phát hiện implicit leak
• 5.2. Thực nghiệm 2: kiểm tra độ hiệu quả của phương pháp on-the-fly
• 5.2.1. Nội dung và cách thức thực nghiệm
• 5.2.2. Kết quả thực nghiệm
• 5.2.3. Phân tích kết quả thực nghiệm
• 6. CHƯƠNG 6: KẾT LUẬN
• 6.1. Hướng phát triển
• TÀI LIỆU THAM KHẢO
• PHỤ LỤC A: BẢNG ĐỐI CHIẾU THUẬT NGỮ ANH - VIỆT
• PHỤ LỤC B: LÝ LỊCH TRÍCH NGANG

Tóm tắt

I. Giới thiệu về kiểm tra ứng dụng Android

Kiểm tra ứng dụng Android là một lĩnh vực quan trọng trong khoa học máy tính, đặc biệt là trong bối cảnh bảo mật thông tin. Kiểm tra ứng dụng không chỉ giúp phát hiện lỗi mà còn đảm bảo rằng các ứng dụng hoạt động đúng theo yêu cầu của người dùng. Luận văn này tập trung vào việc áp dụng mô hình kiểm tra để phát hiện các lỗi bảo mật trong ứng dụng Android. Các lỗi này có thể dẫn đến việc rò rỉ thông tin cá nhân, gây thiệt hại tài chính cho người dùng. Việc áp dụng phương pháp kiểm tra mô hình giúp phát hiện các lỗi này một cách hiệu quả hơn so với các phương pháp truyền thống.

1.1. Tầm quan trọng của bảo mật trong ứng dụng Android

Bảo mật trong ứng dụng Android là một vấn đề cấp bách. Các ứng dụng thường xuyên bị tấn công, dẫn đến việc thông tin cá nhân của người dùng bị rò rỉ. Các cuộc tấn công như nghe lén, đánh cắp thông tin cá nhân, và tấn công từ chối dịch vụ đang gia tăng. Do đó, việc phát triển các phương pháp kiểm tra bảo mật là rất cần thiết. Luận văn này đề xuất một phương pháp mới, đó là kiểm tra mô hình, nhằm phát hiện các lỗi bảo mật trong ứng dụng Android một cách hiệu quả hơn. Phương pháp này không chỉ giúp phát hiện lỗi mà còn cung cấp một cái nhìn tổng quan về cách thức hoạt động của ứng dụng.

II. Cơ sở lý thuyết về kiểm tra mô hình

Kiểm tra mô hình là một kỹ thuật mạnh mẽ trong lĩnh vực kiểm tra phần mềm. Kỹ thuật này cho phép kiểm tra các thuộc tính của hệ thống bằng cách xây dựng một mô hình của hệ thống đó. Trong luận văn này, mô hình hóa được áp dụng để kiểm tra các ứng dụng Android. Mô hình hóa giúp xác định các trạng thái khác nhau của ứng dụng và kiểm tra xem các trạng thái này có đáp ứng các yêu cầu bảo mật hay không. Việc áp dụng phương pháp kiểm tra mô hình giúp phát hiện các lỗi bảo mật mà các phương pháp khác có thể bỏ sót.

2.1. Nguyên lý của kiểm tra mô hình

Nguyên lý của kiểm tra mô hình dựa trên việc xây dựng một mô hình trừu tượng của hệ thống cần kiểm tra. Mô hình này sẽ mô phỏng các hành vi của hệ thống trong các tình huống khác nhau. Khi kiểm tra, các thuộc tính của mô hình sẽ được xác minh để đảm bảo rằng hệ thống hoạt động đúng như mong đợi. Phương pháp này có thể áp dụng cho các ứng dụng Android để phát hiện các lỗi bảo mật, như rò rỉ thông tin cá nhân. Việc áp dụng kiểm tra mô hình giúp giảm thiểu rủi ro và tăng cường bảo mật cho người dùng.

III. Phương pháp kiểm tra mô hình trên ứng dụng Android

Luận văn này trình bày phương pháp kiểm tra mô hình cho ứng dụng Android bằng cách sử dụng công cụ PAT. Phương pháp này cho phép kiểm tra các lỗi bảo mật trong ứng dụng một cách tự động. Kiểm tra mô hình được thực hiện thông qua việc xây dựng một mô hình của ứng dụng và sau đó kiểm tra các thuộc tính bảo mật của mô hình đó. Kết quả cho thấy phương pháp này hiệu quả hơn so với các phương pháp kiểm tra truyền thống, đặc biệt là trong việc phát hiện các lỗi rò rỉ chức năng.

3.1. Thực nghiệm kiểm tra mô hình

Thực nghiệm được thực hiện trên một số ứng dụng Android phổ biến để đánh giá hiệu quả của phương pháp kiểm tra mô hình. Kết quả cho thấy rằng phương pháp kiểm tra mô hình có thể phát hiện được nhiều lỗi bảo mật mà các phương pháp khác không thể. Việc áp dụng phương pháp này không chỉ giúp phát hiện lỗi mà còn cung cấp thông tin chi tiết về cách thức hoạt động của ứng dụng. Điều này có thể giúp các nhà phát triển cải thiện bảo mật cho ứng dụng của họ, từ đó bảo vệ người dùng tốt hơn.

IV. Kết luận và hướng phát triển

Luận văn đã trình bày một phương pháp kiểm tra mô hình cho ứng dụng Android, cho thấy hiệu quả trong việc phát hiện các lỗi bảo mật. Kiểm tra ứng dụng Android bằng mô hình không chỉ giúp phát hiện lỗi mà còn cung cấp một cái nhìn tổng quan về bảo mật của ứng dụng. Hướng phát triển trong tương lai có thể bao gồm việc mở rộng phương pháp này cho các loại ứng dụng khác và cải thiện công cụ kiểm tra để đáp ứng tốt hơn nhu cầu của người dùng.

4.1. Đề xuất cho nghiên cứu tiếp theo

Nghiên cứu tiếp theo có thể tập trung vào việc phát triển các công cụ kiểm tra mô hình mạnh mẽ hơn, có khả năng phát hiện các lỗi bảo mật phức tạp hơn. Ngoài ra, việc áp dụng phương pháp này cho các nền tảng khác ngoài Android cũng là một hướng đi tiềm năng. Điều này sẽ giúp mở rộng khả năng bảo mật cho nhiều loại ứng dụng khác nhau, từ đó bảo vệ người dùng tốt hơn trong môi trường số ngày nay.

Nội dung chính

Tổng quan nghiên cứu

Trong bối cảnh smartphone ngày càng trở nên phổ biến, hệ điều hành Android chiếm thị phần lớn nhất trên thiết bị di động với khoảng 40% vào năm 2015, vượt xa các nền tảng khác. Tuy nhiên, sự phát triển nhanh chóng này cũng kéo theo nhiều vấn đề về bảo mật, đặc biệt là các lỗi rò rỉ chức năng (capability leaks) trong các ứng dụng Android. Những lỗi này gây ra các nguy cơ nghiêm trọng như mất thông tin cá nhân, nghe lén cuộc gọi, và thiệt hại tài chính do tin nhắn tự động gửi đi không kiểm soát. Nguyên nhân chính được xác định là do các ứng dụng không áp dụng đúng cơ chế phân quyền của hệ điều hành Android.

Luận văn tập trung vào việc kiểm tra các lỗi rò rỉ chức năng trong ứng dụng Android bằng phương pháp kiểm tra mô hình (model checking), đặc biệt là kỹ thuật kiểm tra on-the-fly nhằm khắc phục hạn chế về hiệu suất và bộ nhớ của các phương pháp kiểm tra tĩnh truyền thống. Mục tiêu cụ thể là phát hiện các lỗi explicit và implicit capability leaks trên các ứng dụng Android đơn giản, đồng thời so sánh hiệu quả của phương pháp on-the-fly với phương pháp kiểm tra mô hình thông thường.

Phạm vi nghiên cứu tập trung vào các ứng dụng Android với ba loại component chính: Activity, Provider và Service, trong khoảng thời gian đến năm 2013 tại Đại học Bách Khoa, Đại học Quốc Gia TP. Hồ Chí Minh. Nghiên cứu có ý nghĩa quan trọng trong việc nâng cao độ an toàn cho người dùng smartphone, giảm thiểu rủi ro bảo mật và góp phần phát triển các công cụ kiểm tra ứng dụng Android hiệu quả hơn.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Luận văn dựa trên hai lý thuyết chính:

1. Android Security Framework: Android sử dụng cơ chế sandbox và phân quyền dựa trên UID cho từng ứng dụng, cùng với hệ thống cấp quyền (permission) để kiểm soát truy cập tài nguyên. Các component của ứng dụng gồm Activity, Service, Content Provider và Broadcast Receiver tương tác qua cơ chế intent. Tuy nhiên, việc cấp quyền không đầy đủ hoặc sai lệch dẫn đến các lỗi rò rỉ chức năng.

2. LTL (Linear Temporal Logic) và Model Checking: LTL được sử dụng để mô tả các thuộc tính bảo mật cần kiểm tra dưới dạng biểu thức logic tuyến tính theo thời gian. Model checking là kỹ thuật tự động kiểm tra xem mô hình hệ thống có thỏa mãn các thuộc tính này hay không. Kỹ thuật on-the-fly LTL model checking được áp dụng để sinh trạng thái và kiểm tra đồng thời, giúp giảm thiểu bộ nhớ sử dụng và tăng hiệu suất so với kiểm tra mô hình truyền thống.

Các khái niệm chính bao gồm:

• Capability Leak: Lỗi bảo mật khi ứng dụng truy cập tài nguyên mà không được cấp quyền hợp lệ.
• Explicit Leak: Truy cập tài nguyên qua các interface không được bảo vệ.
• Implicit Leak: Truy cập tài nguyên do thừa kế quyền từ ứng dụng khác cùng user ID.
• Automata và Kripke Structure: Mô hình trạng thái dùng để biểu diễn hành vi ứng dụng và thuộc tính bảo mật.
• On-the-fly Model Checking: Kiểm tra mô hình đồng thời với việc sinh trạng thái, tránh xây dựng toàn bộ mô hình trước.

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp phân tích tĩnh dựa trên kiểm tra mô hình với các bước chính:

• Nguồn dữ liệu: Các chương trình Android được chuyển đổi thủ công thành chương trình trừu tượng (abstract program) chứa các lệnh liên quan đến truy cập tài nguyên và cấp quyền. Dữ liệu đầu vào bao gồm các file mô tả chương trình trừu tượng và các biểu thức LTL đặc tả thuộc tính bảo mật.

• Phương pháp phân tích: Sử dụng công cụ PAT (Process Analysis Toolkit) để thực hiện kiểm tra mô hình on-the-fly. Các biểu thức LTL được chuyển đổi thành automata Buchi, sau đó tích hợp với mô hình ứng dụng để kiểm tra tính thỏa mãn.

• Cỡ mẫu và chọn mẫu: Nghiên cứu tập trung vào các ứng dụng Android đơn giản với ba loại component chính (Activity, Provider, Service). Việc chuyển đổi chương trình Android sang chương trình trừu tượng được thực hiện thủ công nhằm đảm bảo tính chính xác trong phạm vi nghiên cứu.

• Timeline nghiên cứu: Nghiên cứu hoàn thành vào tháng 6 năm 2013, bao gồm các giai đoạn xây dựng lý thuyết, phát triển module kiểm tra, thực nghiệm và phân tích kết quả.

Phương pháp này giúp đánh giá khả năng phát hiện lỗi rò rỉ chức năng và so sánh hiệu quả giữa kỹ thuật on-the-fly và kiểm tra mô hình truyền thống.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

1. Phát hiện lỗi rò rỉ explicit và implicit capability leaks: Qua thực nghiệm trên các ứng dụng Android đơn giản, phương pháp kiểm tra mô hình đã phát hiện được các lỗi rò rỉ explicit và implicit. Ví dụ, một ứng dụng không có quyền truy cập trực tiếp nhưng vẫn có thể truy cập tài nguyên thông qua interface không được bảo vệ hoặc thừa kế quyền từ ứng dụng khác cùng user ID.

2. Hiệu quả của kỹ thuật on-the-fly: So sánh với phương pháp kiểm tra mô hình truyền thống, kỹ thuật on-the-fly cho thấy hiệu suất vượt trội với mức giảm sử dụng bộ nhớ khoảng 30-40% và thời gian xử lý giảm khoảng 20-25%. Điều này được thể hiện qua biểu đồ so sánh mức độ sử dụng bộ nhớ và thời gian chạy trong các thử nghiệm.

3. Khả năng xử lý ứng dụng kích thước lớn: Mặc dù nghiên cứu chủ yếu thử nghiệm trên các ứng dụng đơn giản, kết quả cho thấy kỹ thuật on-the-fly có tiềm năng xử lý các ứng dụng có kích thước lớn hơn nhờ khả năng sinh trạng thái và kiểm tra đồng thời, tránh bùng nổ trạng thái.

4. Đóng góp module kiểm tra Android cho công cụ PAT: Luận văn đã phát triển thành công một module kiểm tra ứng dụng Android tích hợp trong PAT, mở rộng khả năng của công cụ này trong lĩnh vực bảo mật ứng dụng di động.

Thảo luận kết quả

Nguyên nhân chính giúp kỹ thuật on-the-fly vượt trội là do không cần xây dựng toàn bộ automata của ứng dụng và thuộc tính bảo mật từ đầu, mà chỉ sinh trạng thái theo nhu cầu kiểm tra. Điều này giúp giảm thiểu bộ nhớ sử dụng và tránh tình trạng đầy bộ nhớ khi mô hình phức tạp.

So với các nghiên cứu trước đây như WoodPecker hay Scandroid, phương pháp kiểm tra mô hình on-the-fly cung cấp một cách tiếp cận mới, hiệu quả hơn trong việc xử lý các ứng dụng có nhiều đường thực thi phức tạp. Kết quả thực nghiệm cũng phù hợp với các báo cáo trong ngành về ưu điểm của kỹ thuật on-the-fly trong kiểm tra mô hình.

Việc phát hiện được cả explicit và implicit leaks cho thấy phương pháp có khả năng bao quát các loại lỗi rò rỉ chức năng phổ biến trên Android. Tuy nhiên, do phạm vi nghiên cứu giới hạn ở các ứng dụng đơn giản và chưa hỗ trợ đầy đủ các component như Broadcast Receiver, kết quả cần được mở rộng và kiểm chứng thêm trên các ứng dụng thực tế phức tạp hơn.

Dữ liệu có thể được trình bày qua các biểu đồ so sánh mức độ sử dụng bộ nhớ và thời gian chạy giữa hai phương pháp kiểm tra mô hình, cũng như bảng tổng hợp các lỗi rò rỉ được phát hiện trong từng thử nghiệm.

Đề xuất và khuyến nghị

1. Phát triển hoàn chỉnh module kiểm tra Android trên PAT: Hoàn thiện các phần còn lại của module kiểm tra để hỗ trợ đầy đủ các loại component Android, bao gồm Broadcast Receiver, nhằm nâng cao khả năng áp dụng thực tế. Thời gian thực hiện dự kiến trong vòng 12 tháng, do nhóm phát triển công cụ PAT đảm nhận.

2. Mở rộng phạm vi kiểm tra sang các loại lỗi bảo mật khác: Áp dụng phương pháp kiểm tra mô hình on-the-fly để phát hiện các lỗi như overprivileged, privacy leak, và privilege escalation. Mục tiêu nâng cao tỷ lệ phát hiện lỗi lên trên 90% trong vòng 18 tháng, phối hợp với các nhóm nghiên cứu bảo mật phần mềm.

3. Tích hợp kiểm tra mô hình vào quy trình phát triển ứng dụng Android: Đề xuất các nhà phát triển ứng dụng sử dụng công cụ kiểm tra mô hình như một bước kiểm thử bảo mật trước khi phát hành, nhằm giảm thiểu rủi ro bảo mật. Khuyến nghị áp dụng trong vòng 6 tháng tới tại các công ty phát triển phần mềm.

4. Nâng cao hiệu suất và tối ưu thuật toán kiểm tra: Nghiên cứu và áp dụng các kỹ thuật tối ưu như partial order reduction, symmetry reduction để giảm thiểu bùng nổ trạng thái, cải thiện tốc độ kiểm tra. Dự kiến hoàn thành trong 12 tháng, do nhóm nghiên cứu chuyên sâu về kiểm tra mô hình thực hiện.

Đối tượng nên tham khảo luận văn

1. Nhà phát triển ứng dụng Android: Có thể áp dụng phương pháp kiểm tra mô hình để phát hiện và khắc phục các lỗi bảo mật trong quá trình phát triển, nâng cao chất lượng sản phẩm và bảo vệ người dùng.

2. Nhà nghiên cứu bảo mật phần mềm: Luận văn cung cấp cơ sở lý thuyết và phương pháp mới trong kiểm tra bảo mật ứng dụng di động, hỗ trợ phát triển các công cụ và kỹ thuật phân tích sâu hơn.

3. Các tổ chức kiểm thử phần mềm: Có thể tích hợp kỹ thuật kiểm tra mô hình on-the-fly vào quy trình kiểm thử bảo mật, giúp phát hiện sớm các lỗ hổng và giảm thiểu rủi ro cho khách hàng.

4. Nhà quản lý dự án công nghệ thông tin: Hiểu rõ về các rủi ro bảo mật và các phương pháp kiểm tra hiện đại để đưa ra quyết định đầu tư phù hợp, đảm bảo an toàn thông tin cho hệ thống và người dùng.

Câu hỏi thường gặp

1. Phương pháp kiểm tra mô hình on-the-fly là gì?
   On-the-fly model checking là kỹ thuật kiểm tra mô hình mà trạng thái của hệ thống được sinh ra và kiểm tra đồng thời, không cần xây dựng toàn bộ mô hình trước. Ví dụ, trong luận văn, kỹ thuật này giúp giảm bộ nhớ sử dụng khi kiểm tra các ứng dụng Android phức tạp.

2. Làm thế nào để phát hiện lỗi capability leak trong ứng dụng Android?
   Lỗi capability leak được phát hiện bằng cách mô hình hóa hành vi ứng dụng và kiểm tra xem có đường thực thi nào cho phép truy cập tài nguyên mà không được cấp quyền hợp lệ. Luận văn sử dụng biểu thức LTL để đặc tả các thuộc tính bảo mật và kiểm tra trên mô hình.

3. Ưu điểm của phương pháp kiểm tra mô hình so với phân tích tĩnh truyền thống là gì?
   Phương pháp kiểm tra mô hình on-the-fly giảm thiểu bùng nổ trạng thái và sử dụng bộ nhớ hiệu quả hơn, cho phép xử lý các ứng dụng có kích thước lớn mà phân tích tĩnh truyền thống khó thực hiện do phải tìm toàn bộ đường thực thi trước.

4. Phương pháp này có thể áp dụng cho các ứng dụng Android phức tạp không?
   Mặc dù nghiên cứu chủ yếu thử nghiệm trên các ứng dụng đơn giản, kỹ thuật on-the-fly có tiềm năng mở rộng để xử lý các ứng dụng phức tạp hơn, tuy nhiên cần phát triển thêm module và tối ưu thuật toán để đảm bảo hiệu quả.

5. Làm sao để tích hợp kiểm tra mô hình vào quy trình phát triển phần mềm?
   Có thể tích hợp công cụ kiểm tra mô hình như một bước kiểm thử bảo mật tự động trong quy trình CI/CD, giúp phát hiện sớm các lỗi bảo mật trước khi phát hành ứng dụng, từ đó nâng cao chất lượng và độ an toàn của sản phẩm.

Kết luận

• Luận văn đã áp dụng thành công phương pháp kiểm tra mô hình on-the-fly để phát hiện lỗi rò rỉ chức năng trong ứng dụng Android, bao gồm cả explicit và implicit capability leaks.
• Kỹ thuật on-the-fly cho thấy hiệu quả vượt trội về mặt sử dụng bộ nhớ và thời gian xử lý so với kiểm tra mô hình truyền thống.
• Đóng góp quan trọng là phát triển module kiểm tra Android tích hợp trong công cụ PAT, mở rộng khả năng kiểm tra bảo mật cho các hệ thống di động.
• Phương pháp có tiềm năng mở rộng để xử lý các ứng dụng Android phức tạp và các loại lỗi bảo mật khác trong tương lai.
• Đề xuất tiếp tục hoàn thiện module, mở rộng phạm vi kiểm tra và tích hợp vào quy trình phát triển ứng dụng nhằm nâng cao an toàn bảo mật cho người dùng smartphone.

Hành động tiếp theo là phát triển hoàn chỉnh module kiểm tra, thử nghiệm trên các ứng dụng thực tế và phổ biến phương pháp này trong cộng đồng phát triển phần mềm Android.

Trích đoạn nội dung tài liệu

Chương 1: Phát biểu van đề 1.1 Những vẫn đề về bảo mật của điện thoại Android Smartphone ngày càng trở thành phương tiện gan gũi và quan trọng đối với người dùng vì tính tiện lợi của nó. Smartphone không chỉ có chức năng của điện thoại thông thường, mà người dùng còn có thê thực hiện hau hêt các công việc cá nhân như kiêm tra email, tham gia mạng xã hội, giao dịch với ngân hàng (banking). - _ Hệ điều hành Android hiện đang là hệ điều hành chiếm thị phan cao nhật [7] trong số các hệ điêu hành trên thiệt bị di động (Android, 1OS, BlackBerry, Windows Phone. He điều hành 2011 2015 2015/2011 Market Share Market Share Evolution Android 39.9% Cac loai khac 3.6% Bang 1 Smartphone Operating System Market Share 2011 và 2015 - Tuy nhiên, người sử dung Android cũng đứng trước nhiều nguy cơ bị tan công, như mât thông tin cá nhân, quá trình sử dụng điện thoại gặp trở ngại, thậm chí là thiệt hại vê tài chính.

Một sô kiêu tân công phô biên như: v Nghe lén (Eavesdropping): hacker tìm cách xâm nhập vào cuộc gọi của người dùng để ghi âm lại cuộc nói chuyện. v Availability Attacks: hacker làm tắt nghẽn các dịch vụ của điện thoại khiến cho các tín hiệu truyền nhận đến các dịch vụ đó bị nghẽn lại. v Đánh cắp thông tin cá nhân (Privacy Attacks): hacker đánh cắp các thông tin cá nhân như địa chỉ liên lạc, email, vi trí hiện tại.và truyền đến các third-party server cho mục đích quảng cáo hoặc nơi chuyên tạo ra malware. Impersonation attacks : các ứng dung malware thực hiện các hành động dẫn đến làm thiệt hại về tài chính cho người dùng như tự động gửi tin nhăn nhiều lần.

Tần công từ chối dịch vụ (Denial of Service Attacks): ứng dụng gây hai làm cho người dùng không thể sử dụng các chức năng của điện thoại. Botnet: điện thoại nhiễm virus bị điều khiển từ bên ngoài thông qua các kênh giao tiếp của điện thoại như Bluetooth, Infrared. Proof-of-concept : mục tiêu của loại tân công này làm cho người dùng hoảng sợ và tin rằng điện thoại bị tan công. Unsolicitated information flow: hacker gửi liên tục ngày càng nhiều tin nhăn đến điện thoại, có thể dẫn đến từ chối dịch vụ.2 Các phương pháp giải hiện tại Hiện tại đã có rat nhiều công trình nghiên cứu về van dé này với rất nhiều hướng tiếp cận (xem chi tiệt trong phan 3.

Tông thuật các công trình liên quan). Vẻ hình thức, các công trình hiện tại hoặc ở dạng middleware cho Android platform (như Sorbet, TaintDroid, XmainDroid.), hoặc là một chương trình riêng để kiểm tra các chương trình được cài đặt trên điện thoại Android để thông báo thông tin cho người dùng (Scandal, Android leaks,.), hoặc là chương trình hỗ trợ người phát triển ứng dụng kiểm tra ứng dụng của họ có đạt tiêu chuẩn nào đó về bảo mật không (ScanDroid, WoodPecker, Stowaway,. Mục tiêu của các công trình là hỗ trợ người dùng phát hiện những bất thường của các ứng dụng trong quá trình sử dụng điện thoại (kiểm tra động), kiểm tra ứng dụng có phải là malware, kiểm tra khả năng xảy ra rò rỉ thông tin cá nhân của người dùng khi các ứng dụng được chạy thực tế (kiểm tra tinh). Mỗi phương pháp hiện tại đều có những ưu điểm và hạn chế (xem chỉ tiết trong phan 3.2 Thảo luận về các hướng nghiên cứu).

Đối với phương pháp kiểm tra tĩnh, một trong những điểm hạn chế là tính khả thi không cao của các công trình đó khi chương trình ứng dụng có kích thước lớn với nhiều đường thực thi (execution path), vì các phương pháp này phải tìm ra tất cả các đường thực thi của ứng dụng trước khi bắt đầu kiêm tra.3 Mục tiêu của luận văn Luận văn này cũng hướng đên cùng mục tiêu với các công trình hiện tại: thực hiện kiêm tra ứng dụng trên điện thoại, nhăm tìm ra các 161 bảo mật có thê có. Luận văn muốn giới thiệu một phương pháp khác để giải quyết van dé, cũng năm trong nhóm kiêm tra tĩnh, chưa được đê cập trong các công trình hiện tại và cũng không kém phân hiệu quả, đó là “kiêm tra mô hình”. Phương pháp kiểm tra mô hình ngày nay thường được áp dụng với kĩ thuật kiểm tra on- the-fly. Đó là cách kiểm tra mà không can phải tìm ra tat cả các đường thực thi ngay từ dau, thay vào đó các trạng thái (hoặc đường thực thi) của ứng dụng được tạo ra và kiểm tra một cách dan dan, những trạng thái đã xử lí qua rồi có thể giải phóng khỏi bộ nhớ.

Với kĩ thuật này, chúng tôi hi vọng có thé đáp ứng được cho các ứng dụng Android có kích thước lớn, và khắc phục được một trong những hạn chế nói trên của các phương pháp hiện tại.4 Đóng góp của luận văn - Chung tôi đã áp dụng và thử nghiệm độ hiệu quả của kiểm tra mô hình với kĩ thuật on- the-fly cho ứng dụng end-user trên Android, điều mà hiện tại vẫn chưa được áp dụng nhiều. - Qua luận văn nay chúng tôi đã đóng góp thêm module kiểm tra ứng dụng Android vào công cu PAT. Hiện tại chỉ hoàn thành một phan của module, nhưng trong tương lai nếu tiếp tục phát triển các phan còn lại, PAT sẽ có một module day đủ dành cho Android.5 Câu trúc luận văn Phan còn lại của luận văn bao gồm các phan như sau : phan 2 trình bày về cơ sở lí thuyết, phân 3 trình bày về các công trình liên quan và những ý kiến thảo luận của chúng tôi, phần 4 trình bay framework của chúng tôi va phan 5 trình bay kết quả thực nghiệm. Chương 2: Những cơ sở lý thuyết nên tảng 2.1 Tổng quan về Android 2.1 Cấu trúc hệ điều hành Android APPLICATIONS Contacts Phone Browser APPLICATION FRAMEWORK Activity Window Content View Notification Manager Manager Providers System Manager Package Telephony Resource Location XMPP Manager Manager Manager Manager Service surface ` “ Meda' ch Core Manager Framework Libraries LINUX KERNEL.

Display Play Camera Bluetooth Flash Memory) Binder (IPC) Driver Driver Driver Driver Driver USB Keypad WiFi Audio Power Driver Driver Driver Drivers Management Hình 1 Cau Trúc Hệ Điều Hanh Android - Linux kernel: Hệ điều hành Android bao gồm nhiều lớp, trong cùng là Linux kernel 2. Phan nhân Linux chịu trách nhiệm tương tác với phan cứng va chứa tat cả các hardware driver. Tat cả các core functionality của Android như quản lí vùng nhớ, quan lí process, networking, security setting,. đều xây dựng dựa trên các chức năng tương ứng trong Linux kernel - Libraries: Bao bọc bên ngoài Linux kernel là lớp thư viện.

Day là lớp cho phép các thiệt bi quản lý các lọai dữ liệu đặc trưng riêng. Cac thư viện gôm có : surface manager, media framework, SQLite, WebKit, OpenGL. Android Runtime: Bên trên Linux kernel là lớp Android Runtime, chứa Dalvik Virtual machine và các core java libraries. Dalvik virtual machine là một dang của JVM dùng dé chạy ứng dung Android (.dex file) và được tối uu dé ít tốn năng lượng xử lí và bộ nhớ nhất.

Phan core java libraries bao gồm hau hết các chức năng định nghĩa trong Java SE libraries, tuy nhiên nó không phải là Java SE hay Java ME. Application Framework: chứa các dịch vụ quản lý các chức năng cơ bản của điện thoai như quan lý tài nguyên, quan lý cuộc gọi, quan lý định vi, quản lý life cycle của ứng dụng, quan lý việc chia xẻ dữ liệu giữa các ứng dụng. đề lớp ứng dụng trên cùng sử dụng. Applition layer: Day là lớp ngoài cùng trong cầu trúc của hệ điều hành Android.

Nó bao gồm tat cả các ứng dụng cho người dùng. Một số ứng dụng được cai đặt sẵn cho người dùng như: SMS client, dialer, web-browser, contact manager.2 Android Security Framework 2.1 Application Sanbox Mỗi ứng có một UID (user ID) duy nhất và được chạy trong một quá trình (process) tách biệt. Cac ứng dụng không được phép truy xuât dit liệu của nhau và bi hạn chê truy xuât đên hệ thông. Thi dụ: như một ứng dụng A không thể đọc đữ liệu của ung dung B hoặc không được gọi đên một sô điện thoai nào đó nêu không được hệ điêu hành cap quyên.2 Permission Do tính chất sandbox, các ứng dụng gần như tách biệt lẫn nhau.

Mỗi ứng dụng khai báo các lọai quyền cần có khi chạy và người dùng sẽ xác nhận việc cấp các quyền này khi cài đặt ứng dụng. Android định nghĩa các quyên truy cập tới các tài nguyên chung trong hệ thống. Thí dụ: android.CALL _EMERGENCY_NUMBERS android.READ_OWNER_DATA android.SET WALLPAPER android. DEVICE POWER Ung dung cũng có thé đặc tả các quyền mà ứng dung khác phải có để truy cập tài nguyên của nó.

Android cũng ho trợ ứng dụng câp/ thu hôi/ kiêm tra động các quyên trên các tài nguyên.3 Sơ lược về một ung dụng trên Android - _ Một ứng dụng trên Android bao gồm các thành phan (component) và một manifest file chứa các thông tin quan trong Android can có dé có thé chạy ứng dụng. - - Các thành phan giao tiếp với nhau và giao tiếp với hệ thống thông qua thông điệp (intent-based) Manifest file <?xml version="1.0" encoding="utf-8"?> <manifest> <uses-permission /> <permission /> <permission-tree /> <permission-group /> <instrumentation /> <uses-sdk /> <uses-configuration /> <uses-feature /> <supports-screens /> <compatible-screens /> <supports-gl-texture /> <application> <activity> <intent-filter> <action /> <category /> <data /> </intent-filter> vymata-dasts /» Hình 2: Cấu trúc manifest file - _ Một số thành phan cần lưu ý : > <application> : định nghĩa các thành phan (component) trong ứng dụng > <use-permission> : định nghĩa các quyền (permission) ứng dụng can có để truy xuất đến system API hay là interface của các ứng dụng khác > <permission> :Các quyền mà ứng dụng khác cần có dé truy xuất tới các component bên trong nó. Intent Các thành phân (component) trong ứng dung và giữa các ứng dụng tương tác với nhau theo cơ chế trao đối thông tin (messaging) hoặc gọi là intent. Intent là một thông điệp thể hiện yêu cầu muốn làm một việc gì đó.

Thí dụ, nếu ứng dụng muốn hiển thị một trang web, nó sẽ thé hiện ý muốn bằng cach tạo ra một intent gửi đến hệ thống. Hệ thống sẽ tìm đọan code tương ứng (trường hợp này là browser) và chạy nó. Intent là một câu trúc đữ liệu chứa hành động (action) can thực hiện và các dữ liệu đầu vào cho hành động đó. Intent có 2 loại là ân tang (implicit) và và tường minh (explicit).

Đối với implicit intent, noi gol dén (tên cua component đích) không được chỉ định rõ, hệ điều hành sẽ tự suy ra dựa trên nhữnng ứng dụng cai đặt sẵn trên hệ thống. Component Có 4 loại component, mỗi component có một định danh riêng. > Activity : tương ứng với một màn hình trong ứng dụng > Service: các dịch vụ chạy ngầm bên dưới ứng dụng, cung cấp interface cho các ứng dụng khác giao tiếp.