Từ một vụ bê bối tại Vương quốc Anh

Tại Vương quốc Anh, một vụ bê bối lớn đã xảy ra và kéo dài nhiều năm, liên quan đến Post Office Limited (POL) và những nhân viên/ đại lý mà họ buộc tội trộm cắp. Bằng chứng chống lại các bị cáo là chênh lệch số dư trong hệ thống phần mềm kế toán. Tại thời điểm đó, các bị cáo khó có thể kêu oan trong quá trình tố tụng. Một phần vì từ năm 1997, Ủy ban Luật pháp Vương quốc Anh khuyến nghị rằng một máy tính nên được coi là hoạt động bình thường trừ khi có bằng chứng rõ ràng khác (khiếu nại của bị đơn rằng hệ thống có lỗi không được xét tới).

Ở Hoa Kỳ, tình hình có phần hơi khác do các bị cáo có thể yêu cầu tiếp cận bằng chứng. Thẩm phán Stephen Smith đã trình bày chi tiết trong Tạp chí Luật Hình sự Hoa Kỳ (American Criminal Law Review) năm 2017, các tòa án liên bang ngày càng coi trọng cái gọi là “đặc quyền thực thi pháp luật”, họ có thể từ chối cung cấp thông tin về các kỹ thuật thu thập bằng chứng trong phiên tòa và điều đó có thể mở rộng tới phần mềm, ngăn cản việc xem xét các lỗi phần mềm.

Cách làm ở cả hai quốc gia trên đều cần được xem xét lại. POL có thể là nhà bán lẻ lớn nhất Vương quốc Anh nhưng đã truy tố nhân viên/ đại lý của mình trong khi chính phần mềm của họ có lỗi. Tình hình ở Hoa Kỳ cũng đáng quan tâm khi tòa án nước này đang nhận thức được khả năng sai sót của phần mềm - một phần là nhờ nỗ lực của giáo sư Susan Landau (đại học Tufts, Hoa Kỳ) và các đồng nghiệp. Các ví dụ ở Vương quốc Anh và Hoa Kỳ nhấn mạnh sự nguy hiểm khi dựa vào phần mềm, kiểm tra DNA, phân tích pháp y máy tính… với tư cách là chứng cứ và các cách mà tòa án có thể xử lý vấn đề này.

POL là một doanh nghiệp lớn với 17.000 chi nhánh, cung cấp nhiều dịch vụ ngoài việc bán tem và các gói vận chuyển. Các chi nhánh nhỏ của bưu điện - các bưu cục phụ - được điều hành bởi các nhân viên tự kinh doanh. Các bưu cục nhỏ như vậy thường phát triển mạnh nhờ liên hệ cá nhân. Vì vậy, không có gì đáng ngạc nhiên khi những người đại lý bưu điện tự doanh (subpostmaster - SPM) tạo thành một phần cấu trúc cộng đồng của POL.

Từ năm 2000-2014, POL đã phát hiện sự thiếu hụt trong tài khoản của nhiều SPM. Một số tài khoản thiếu hàng trăm bảng Anh, một số khác thiếu hàng ngàn bảng Anh. Các SPM không thể tìm ra lý do cho những sự thiếu hụt và không được POL đưa ra lời giải thích. Trên thực tế, có nhiều loại lỗi đồng bộ khác nhau trong phần mềm. Một vấn đề điển hình là giao dịch được ghi nhận tại bưu cục nhưng không được ghi nhận ở hệ thống trung tâm.

Các vấn đề bắt đầu từ năm 1999, thời điểm POL áp dụng hệ thống phần mềm phân tán Horizon IT. Khi các SPM phàn nàn rằng các tài khoản trung tâm bị lỗi, POL đã tiến hành một cuộc điều tra nội bộ, nhưng không kiểm tra nhật ký giám sát (audit log) để xác định điều gì đã xảy ra. Kết luận cho rằng vấn đề xuất phát do SPM.

Nhưng đối với các SPM, vấn đề này có tính nghiêm trọng hơn. Điểm nổi bật nhất theo góc nhìn của Hoa Kỳ là trong hệ thống pháp luật của Anh, một số tổ chức tư nhân nhất định có thể đóng vai trò công tố. POL đã buộc tội 918 SPM về hành vi trộm cắp. Nhiều người đã phải vào tù. Một số bị mất nhà cửa và lương hưu. Những người khác đã phá sản khi trả tiền theo yêu cầu của POL. Các SPM đã không thể tự vệ một cách hiệu quả, không hiểu rõ về nguyên nhân vụ việc và không được POL trợ giúp.Trên thực tế, nhiều vụ thiếu hụt tài khoản SPM không liên quan gì đến hành vi trộm cắp, mà là kết quả của lỗi phần mềm. Thật vậy, cho đến năm 2018, POL đã che giấu thông tin về “Nhật ký lỗi đã biết” (danh mục các lỗi đã biết và cách giải quyết trong hệ thống công nghệ, do Fujitsu - công ty cung cấp phần mềm Horizon duy trì) với các SPM và tòa án. Những vấn đề với phần mềm chỉ được phát hiện sau khi các SPM kiện POL ra tòa và được điều tra kỹ.

Tháng 12/2019, thẩm phán Fraser của Tòa Nữ hoàng thuộc Tòa án Tư pháp Cấp cao (Queen's Bench Division of the High Court of Justice) đã phán quyết: “Có thể lỗi, sai sót hoặc khiếm khuyết... gây ra sự sai lệch rõ ràng hay bị cáo buộc hoặc sự thiếu hụt liên quan đến tài khoản hoặc giao dịch của các SPM... tất cả bằng chứng trong phiên tòa Horizon Issues không chỉ cho thấy điều này có khả năng xảy ra, mà nó thực sự đã xảy ra và xảy ra trong nhiều lần”.

Lỗi đã xảy ra nhiều lần và trong nhiều trường hợp khác nhau: đôi khi phần mềm Horizon thể hiện là giao dịch đã được thực hiện trong khi thực tế điều đó không xảy ra (giao dịch bị dừng lại giữa chừng) và trong những lần khác, giao dịch không được hoàn thành chính xác.

Ủy ban Rà soát các vụ xét xử hình sự (CCRC), một hội đồng độc lập xem xét các vụ oan sai ở Anh, xứ Wales và Bắc Ai-len, bắt đầu điều tra các vấn đề đó năm 2015. CCRC xem xét các vụ kháng cáo chỉ khi bằng chứng mới được phát hiện có thể lật ngược bản án. Các lỗi, sai sót và khiếm khuyết phần mềm được phát hiện đáp ứng điều kiện đó và CCRC đã chuyển nhiều vụ kiện của SPM lên Tòa phúc thẩm và Tòa án Hoàng gia.

CCRC đã nhận được 61 đơn từ các SPM bị kết án. Tháng 01/2021, CCRC đã chuyển vụ kiện của 51 người trong số đó đến các tòa phúc thẩm phù hợp. Sáu bản án đã được lật lại và POL cho biết sẽ không phản đối 38 vụ khác.

Khi vụ án Horizon IT đang dần được xử lý tại các tòa án vào năm 2020, 04 chuyên gia về độ tin cậy của các hệ thống dựa trên phần mềm là Peter Ladkin, Bev Littlewood, Harold Thimbleby và Martyn Thomas đã viết “với bất kỳ hệ thống máy tính dựa trên phần mềm phức tạp tương đối nào, chẳng hạn như hệ thống xử lý giao dịch CNTT Horizon... thực tế không thể phát triển một hệ thống sao cho tính đúng đắn của mọi hoạt động phần mềm có thể được chứng minh theo tiêu chuẩn liên quan trong tố tụng pháp lý”. Từ đó, họ khuyến nghị các tòa án nên cho rằng bất kỳ hệ thống phần mềm nào cũng có thể có lỗi. Điều này làm thay đổi câu hỏi liên quan trước tòa, “bằng chứng có thể bị lỗi máy tính gây ảnh hưởng nghiêm trọng đến mức nào?”

Các kỹ sư phần mềm đề xuất một bài kiểm tra ba phần. Trước tiên, tòa án phải có quyền truy cập vào «Nhật ký lỗi đã biết», một phần của bất kỳ dự án phần mềm được phát triển chuyên nghiệp nào. Tiếp theo, tòa án nên xem xét liệu bằng chứng được đưa ra có thể bị ảnh hưởng nghiêm trọng do lỗi phần mềm không. Ladkin và các đồng tác giả lưu ý rằng một chuỗi email qua lại không có khả năng xảy ra lỗi như vậy, nhưng thời gian mà một công cụ phần mềm ghi lại khi một ứng dụng được sử dụng rất có thể không chính xác. Cuối cùng, các chuyên gia khuyến nghị kiểm tra xem liệu mã nguồn có tuân theo tiêu chuẩn công nghiệp được sử dụng trong phiên bản của tác vụ thủ công hay không.

Nhóm kỹ sư này cùng với các luật sư nổi tiếng Paul Marshall và Stephen Mason, luật sư hình sự Jonathan Rogers, chuyên gia kiểm tra và kiểm toán phần mềm James Christie, và nhà thống kê Martin Newby đã điều chỉnh khuyến cáo của Bộ Tư pháp Vương quốc Anh. “Về nguyên tắc, ngưỡng để bác bỏ giả định là thấp, buộc bên dựa vào tài liệu để chứng minh phải có trách nhiệm chứng minh độ tin cậy của tài liệu đó và do đó chứng minh tính toàn vẹn và độ tin cậy của nguồn máy tính của mình”. Đây không phải là tiêu chuẩn đã được áp dụng trong các vụ việc của POL. Các tác giả chỉ trích POL vì đã không tiết lộ sự tồn tại của “Nhật ký lỗi đã biết” trong quá trình tố tụng và kết luận rằng: “mọi chương trình quan trọng sẽ chứa nhiều lỗi khiến nó không thể tạo ra kết quả chính xác khi gặp một số kết hợp dữ liệu đầu vào cụ thể”.

Các nhà nghiên cứu Steven Bellovin, Matt Blaze, Brian Owsley và giáo sư Susan Landau đang xem xét vấn đề tương tự từ góc độ của Hoa Kỳ. Hoa Kỳ không có khuyến nghị về tính đúng đắn của kết quả máy tính, nhưng lại có vấn đề là đặc quyền thực thi pháp luật đang ngày càng tăng lên. Các nhà nghiên cứu tập trung xem xét hậu quả của phần mềm máy tính được sử dụng để tạo bằng chứng khi các hệ thống phức tạp (hệ điều hành, phần mềm và phần cứng) có lỗi và trên thực tế, thường xuyên bị lỗi.

Điều gì xảy ra nếu phần mềm gây ra lỗi và không có mẫu để kiểm tra hoặc nếu phần mềm tự tạo ra bằng chứng? Cho tới tháng 6/2021, không có quy định về việc cơ quan thực thi pháp luật phải cung cấp mã ứng dụng để bị đơn có thể tự kiểm tra.

Đã có rất nhiều trường hợp chứng minh sự phù hợp của một bước đi như vậy. Trong một vụ liên quan đến Máy phân tích hơi thở, vụ Tiểu bang kiện Jane Chun và những người liên quan, những người kiểm tra phần mềm bên ngoài đã tìm ra hàng ngàn lỗi trong mã nguồn của Máy phân tích hơi thở đang sử dụng. Và không chỉ phần mềm thương mại mới có lỗi. Các lỗi tương tự đã dẫn đến việc cấu hình sai thiết bị nghe lén, khiến FBI thu thập thông tin quá mức.

Trong một vụ án tại Hoa Kỳ năm 2014, chuyên gia pháp y máy tính Jonathan Zdziarski đã phát hiện ra rằng các công cụ pháp y máy tính “được sử dụng để đánh giá bằng chứng ban đầu ... đã báo cáo sai bằng chứng hoặc không thừa nhận hoàn toàn sự tồn tại của nó”. Các công cụ thương mại đã báo cáo sai về việc xóa thiết bị và khôi phục sao lưu, ngày sử dụng ứng dụng và thời gian một tệp được truy cập. Thông tin từ Zdzairski đã khiến các cáo buộc nghiêm trọng nhất bị loại bỏ.

Những vấn đề pháp lý khi phần mềm đóng vai trò như một nhân chứng

Trong các trường hợp trên, phần mềm đóng vai trò như một nhân chứng. Điều khoản đối chất của Tu chính án (amendment - bản sửa đổi một số điều của hiến pháp ở một số nước như Mỹ, Đức, Pháp…) thứ sáu trao cho các bị cáo trong các vụ án hình sự quyền được biết bản chất của bằng chứng chống lại họ, và Tòa án Tối cao đã ra phán quyết rằng các bị cáo có quyền đối chất với những người làm chứng chống lại họ, “lời khai của các nhân chứng vắng mặt tại phiên tòa chỉ được chấp nhận khi người khai không có mặt và chỉ khi bị đơn đã có cơ hội kiểm tra chéo trước đó”.

Kể từ năm 1963, theo phán quyết của Tòa án Tối cao trong vụ Brady kiện bang Maryland, bên công tố phải cung cấp cho bị cáo tất cả các bằng chứng có lợi cho bị cáo mà bên công tố sở hữu. Nhưng thẩm phán Smith đã cho thấy các tòa án liên bang đang ngày càng có xu hướng công nhận đặc quyền bảo vệ các kỹ thuật và thủ tục điều tra thực thi pháp luật khỏi bị tiết lộ trước tòa. Tình hình còn tệ hơn do đôi khi cơ quan thực thi pháp luật không thực sự có quyền truy cập vào phần mềm, mã nguồn là độc quyền và cơ quan thực thi pháp luật chỉ nhận được đầu ra. Khi cơ quan thực thi pháp luật không thể truy cập vào phần mềm thì bị đơn sẽ không có quyền truy cập và do đó không thể xác định xem phần mềm có lỗi hay không.

Trong vài thập kỷ qua, các chuyên gia đã có thể sản xuất phần mềm quan trọng theo cách an toàn hơn. Ví dụ như Cơ quan Chỉ đạo các Dự án Nghiên cứu Quốc phòng Tiên tiến của Hoa Kỳ (DARPA) đã phát triển một máy bay trực thăng “không thể hack”. Nhưng các phần mềm thông thường thì dễ có lỗi hơn. Watts Humphrey, nhà nghiên cứu của Đại học Carnegie Mellon, cho biết, trung bình, một nhà phát triển phần mềm có kinh nghiệm gây ra một lỗi sau mỗi mười dòng lệnh. Còn 20% lập trình viên hàng đầu chỉ gây ra 29 lỗi trên một ngàn dòng lệnh. Tuy nhiên, máy phân tích hơi thở có thể có từ 50 đến 100 ngàn dòng lệnh, trong khi các chương trình phức tạp, chẳng hạn như hệ thống Horizon, lớn hơn rất nhiều lần.

Bất kỳ nhà cung cấp phần mềm có trách nhiệm nào cũng kiểm tra toàn diện để xem phần mềm có hoạt động chính xác không trước khi phát hành. Đôi khi lỗi có thể được tìm thấy tương đối dễ dàng nhưng cũng có trường hợp lỗi chỉ được phát hiện bởi người dùng. Đôi khi, cách duy nhất để tìm ra lỗi là xem xét trực tiếp mã nguồn. Cả hai điều này đều có ý nghĩa quan trọng đối với việc sử dụng các chương trình phần mềm trong phòng xử án.

Do tỷ lệ lỗi cao trong các hệ thống phần mềm phức tạp, các chuyên gia kết luận rằng tòa án không thể cho rằng phần mềm cung cấp bằng chứng là đáng tin cậy. Thay vào đó, bên công tố phải cung cấp mã cho các chuyên gia của bị cáo để họ “kiểm tra đối nghịch”. Để tránh trường hợp chính phủ không có mã nguồn, các hợp đồng mua sắm của chính phủ phải yêu cầu cung cấp mã nguồn cho mọi phiên bản của phần mềm.

Những nỗ lực của giáo sư Susan Landau và đồng nghiệp đã có tác động nhất định. Trong phán quyết của Tòa phúc thẩm New Jersey liên quan đến một công nghệ phân tích ADN mới được sử dụng trong một vụ án giết người, Corey Pickett bị cáo buộc là một trong hai tay súng đã bắn vào đám đông, giết chết một người đàn ông và làm bị thương một bé gái. Hai người đàn ông bị bắt sau một cuộc rượt đuổi; ngay sau đó cảnh sát đã tìm thấy một khẩu súng cỡ nòng 0,38 và một chiếc mũ trượt tuyết trên con đường mà họ đã đi. Phân tích DNA truyền thống không thể gắn Pickett với chứng cứ, vì vậy cơ quan thực thi pháp luật đã sử dụng phần mềm TrueAllele DNA để đối chiếu. TrueAllele thực hiện “định dạng gen theo xác suất”, điều phát huy tác dụng khi các nhà điều tra có mẫu trộn lẫn ADN của nhiều người. Tuy nhiên, như tòa án đã lưu ý, một nghiên cứu gần đây của Hội đồng Cố vấn Khoa học và Công nghệ của Tổng thống nhận định rằng công nghệ này vẫn đang phát triển và đòi hỏi “sự giám sát chặt chẽ”.

TrueAllele chưa từng trải qua loại hình giám sát chặt chẽ này. Ngay cả khi lý thuyết đằng sau nó được chứng minh, phần mềm cũng cần được kiểm tra kỹ. Nhấn mạnh những luận điểm về nhu cầu kiểm tra đối nghịch với mã, tòa án phán quyết, "Che giấu mã nguồn không phải là câu trả lời. Giải pháp là sản xuất mã nguồn theo lệnh bảo vệ (protective order). Điều này để bảo vệ quyền sở hữu trí tuệ và quyền lợi hợp pháp của bị đơn là ngang nhau. Luật sở hữu trí tuệ nhằm mục đích ngăn chặn các đối thủ cạnh tranh đánh cắp bí mật thương mại trên thị trường. Nó không bao giờ nhằm biện minh cho việc che giấu thông tin liên quan với các bên trong xét xử hình sự". Quyết định này có giá trị bắt buộc tại các tòa án tiểu bang ở New Jersey.