Các bài kiểm tra dựa trên thuộc tính đơn giản cho trình xác thực Plutus

Các bài kiểm tra dựa trên thuộc tính đơn giản cho trình xác thực Plutus

Cách viết mã off-chain với thư viện ‘cook-validators’ và nhận các bài kiểm tra dựa trên thuộc tính miễn phí

Gần đây, chúng tôi đã nghe Victor Miraldo , người đứng đầu nhóm kiểm toán và xác minh hợp đồng thông minh tại Tweag , về tầm quan trọng của việc xác minh vì lý do bảo mật trong thế giới tài chính phi tập trung (DeFi). Victor là một kỹ sư phương pháp chính thức của Haskell và cam kết đảm bảo tính an toàn và đúng đắn của các ứng dụng phi tập trung (DApps) thông qua các công cụ và quy trình. Trong bài đăng trên blog này, anh ấy phác thảo cách viết và triển khai DApp đơn giản là chưa đủ, và tại sao mọi nhà phát triển nên kiểm tra kỹ lưỡng tất cả mã trên chuỗi và tập lệnh Plutus chống lại một loạt các tác nhân xấu. Vì vậy, anh ấy giới thiệu một thư viện các công cụ làm sẵn để tương tác với các tập lệnh trình xác thực Plutus – được gọi là cook-validators, được phát triển tại Tweag. Thư viện này giúp triển khai lớp trong cùng của mã ngoài chuỗi, lớp này chịu trách nhiệm tạo và gửi các giao dịch. Bằng cách sử dụng thư viện này, bạn có thể nhận miễn phí các bài kiểm tra dựa trên thuộc tính ở cấp độ giao dịch.

Hãy nghe Victor nói gì về việc sử dụng thư viện của họ.

Giới thiệu

Kiểm tra cấp độ giao dịch cho phép chúng tôi gửi các giao dịch tùy ý tới các tập lệnh trình xác thực và để đánh giá hành vi của chúng. Quá trình này khác với việc kiểm tra toàn bộ hợp đồng thông minh bằng cách sử dụng các điểm cuối đã xác định như một phần của mã ngoài chuỗi của hợp đồng. Rốt cuộc, mã off-chain đó được thiết kế để hợp tác liền mạch với mã on-chain và sẽ có các kiểm tra an toàn và bảo mật nội tại của riêng nó. Phương pháp này hoạt động đối với các hoạt động bình thường, nhưng trong thiết lập thử nghiệm, nó thường bảo vệ các tập lệnh trình xác thực trên chuỗi khỏi các đầu vào sai hoặc thậm chí độc hại. Do đó, để kiểm tra cấp độ giao dịch, chúng tôi muốn phá vỡ mã off-chain đang làm sạch và các đoạn mã trên chuỗi có cùng khả năng mà cơ sở hạ tầng off-chain được tạo thủ công của kẻ tấn công có thể mang lại. Tương tự với các dịch vụ web,

Thư cooked-validatorsviện cho phép bạn viết mã off-chain chịu trách nhiệm tạo và gửi các giao dịch và sử dụng cùng một mã để thực hiện và kiểm tra hợp đồng của bạn, ở cấp độ giao dịch. Điều này làm cho việc viết các bài kiểm tra cho chuỗi trực tuyến trở nên dễ dàng hơn nhiều, có thể phát hiện ra một số điều tồi tệ có thể xảy ra hoặc không thể xảy ra.

Giới thiệu về thư viện ‘cook-validators’

Việc xây dựng hợp đồng của bạn với các trình xác thực đã nấu chín không khác nhiều so với những gì bạn đã quen với Contractđơn nguyên. Giả sử bạn đã làm theo hướng dẫn về Hợp đồng phân tách cho đến và bao gồm cả phần ‘Xác định tập lệnh trình xác thực’. Cuối cùng, bạn có một splitValidatorhàm thực thi phần trực tuyến của hợp đồng đó. Nếu bạn không làm theo hướng dẫn, splitValidatorhợp đồng sẽ khóa một số tiền nhất định mà chỉ có thể được mở khóa bằng cách phân chia tiền giữa hai bên đã chỉ định trước đó.

Bây giờ, để tương tác với chính hợp đồng đó, chúng ta cần viết mã ngoài chuỗi , mã này tạo và gửi các giao dịch cần thiết tới chuỗi khối. Thay vì làm điều đó trực tiếp trong Contractđơn nguyên, chúng tôi sẽ dựa vào cooked-validatorsthư viện. Giao lockFundsdịch có thể được viết như sau:

lockFunds :: (MonadBlockChain m) => SplitData -> m ()
lockFunds [email protected]{amount} = void $ validateTxConstr
  [PaysScript splitValidator [(datum, Ada.toValue amount)]]

Điều này rất giống với những lockFunds gì chúng tôi đã viết trong Contractđơn nguyên trực tiếp. Sự khác biệt là ở đây chúng tôi sử dụng đơn nguyên MonadBlockChain tùy ý . Kỹ thuật này cho phép chúng tôi sử dụng giống nhau lockFundscho hai mục đích:

  1. tạo giao dịch, vì Contractđơn nguyên là một phiên bản của MonadBlockChain, và
  2. viết các bài kiểm tra cho các trình xác nhận trên chuỗi bằng cách sử dụng các cơ sở xác nhận đã nấu chín.

Giả sử rằng chúng tôi cũng đã xác định các unlockFundsgiao dịch ( mã để sử dụng ), do đó, điều đó cooked-validatorssẽ tương tác liền mạch với Contractđơn nguyên. Trên thực tế, chúng ta có thể định nghĩa endpointshàm giống như trong hướng dẫn :

endpoints :: (AsContractError e) => Promise w SplitSchema e ()
endpoints = selectList [lock, unlock]
  where
    lock = endpoint @"lock" (lockFunds . mkSplitData)
    unlock = endpoint @"unlock" (const unlockFunds)

Kiểm tra hợp đồng

Bởi vì chúng tôi đã xác định lớp đầu tiên của mã ngoài chuỗi của mình (tạo và gửi các giao dịch thô) cooked-validators, chúng tôi có thể sử dụng cơ sở hạ tầng thử nghiệm của nó để kiểm tra trình xác thực trên chuỗi . Một bài kiểm tra cơ bản về việc có thể mở khóa các khoản tiền đã bị khóa hay không có thể trông như sau:

unlockPossible1 = assertSucceeds $ do
  lockFunds sd `as` wallet 1 -- sends the lockFunds pretending to be user 1,
  unlockFunds `as` wallet 2 -- sends the unlockFunds pretending to be user 2.
where
  -- makes a split of 10 ada between users 2 and 3 that only those users should be able to unlock.
  sd = SplitData (wallet 2) (wallet 3) 10

Ở đây, bộ astổ hợp chỉ hoạt động khi mã thử nghiệm và nó cho phép chúng tôi tương tác với hợp đồng của mình theo cách giống như nhiều người dùng.

Chức năng unlockPossible1là một bài kiểm tra đơn vị để kiểm tra xem có điều gì tốt xảy ra hay không. Chúng tôi có thể dễ dàng kiểm tra rằng điều gì đó xấu không xảy ra:

unlockImpossible1 = assertFails $ do
  lockFunds sd `as` wallet 1
  unlockFunds `as` wallet 5 -- user 5 shouldn't be able to unlock the funds.
where
  sd = SplitData (wallet 2) (wallet 3) 10

Chúng tôi cũng có thể sử dụng các bài kiểm tra này như các bài kiểm tra dựa trên thuộc tính . Trong trường hợp này, thuộc tính đang được kiểm tra là một trong hai người nhận phần tách luôn có thể mở khóa:

unlockProp1 = forAllTr tr assertSucceeds
  where
    tr = do
      -- generates a random SplitData
      sd <- genSplitData
      -- generates a random wallet; anyone can lock funds.
      w <- genArbitraryWallet
      lockFunds sd `as` w
      -- but only the recipients can unlock the funds
      unlocker <- choose [ recipient1 params , recipient2 params ]
      unlockFunds `as` unlocker

Ngoài ra, nếu một trong các thử nghiệm của chúng tôi không thành công, chúng tôi sẽ nhận được một bản tóm tắt có thể đọc được về các giao dịch khiến thử nghiệm không thành công. Dưới đây là đoạn trích của ba giao dịch đầu tiên từ một lần thử nghiệm không thành công của trình xác thực có liên quan hơn:

1) ValidateTxSkel
     - Signers: [wallet #1 (a2c20c)]
     - Label: ProposalSkel 2(Payment{paymentAmount = 4200000,paymentRecipient = a96a66})
     - Constraints:
        /\ Mints
            - (18ab4cc $ "threadToken"): 1
            - Policies: [18ab4c]
        /\ PaysScript script 9d52e00:
            - Accumulator{payment = Payment{paymentAmount = 4200000,paymentRecipient = a96a66},signees = []}
              { Lovelace: 6200000
                (18ab4cc $ "threadToken"): 1 }

2) ValidateTxSkel
     - Signers: [wallet #1 (a2c20c)]
     - Constraints:
        /\ PaysScript script 9d52e00:
            - Sign{signPk = a2c20c,signSignature = 8fef22}
              Lovelace: 1

3) ValidateTxSkel
     - Signers: [wallet #2 (80a4f4)]
     - Constraints:
        /\ PaysScript script 9d52e00:
            - Sign{signPk = 80a4f4,signSignature = 6853e0}
              Lovelace: 1
...

Dấu vết được hiển thị cho nhà phát triển chứa tất cả thông tin cần thiết để gỡ lỗi sự cố và nó cố gắng trình bày thông tin theo cách có thể đọc được.

Ngoài kiểm tra dựa trên tài sản, cooked-validatorscũng cung cấp khả năng sửa đổi các giao dịch theo dõi theo một số chức năng. Điều này có thể mô phỏng một cuộc tấn công theo nhiều cách khác nhau. Ví dụ, viết một bài kiểm tra như:

attackNotPossibleOnSplit = assertFails $ do
  somewhere doAttack $ do
    lockFunds sd `as` wallet 1
    unlockFunds `as` wallet 2
 where
  sd = SplitData (wallet 2) (wallet 3) 10

sẽ gây ra cooked-validatorsviệc cố gắng thực hiện hai thử nghiệm, cả hai đều không thành công, như sau:

  1. sửa đổi lockFunds sdgiao dịch theo doAttack, sau đó gửi; sau đó gửi một chưa sửa đổi unlockFunds hoặc
  2. đệ trình lockFunds sd; sau đó sửa đổi và trình unlockFundstheo doAttack.

Các chi tiết của bộ tổ hợp ở đâu đó có thể hơi phức tạp, do đó chúng tôi sẽ bỏ qua ở đây. Có một bài đăng trên blog riêng đưa ra các chi tiết kỹ thuật trên blog Tweag cho những ai quan tâm.

Thư viện liên quan và kết luận

Mặc dù Plutus đã hỗ trợ một hình thức kiểm tra dựa trên thuộc tính của các điểm cuối hợp đồng với ContractModellớp của nó, nó không cung cấp kiểm tra mức giao dịch. Kiểm tra mức giao dịch là rất quan trọng đối với chúng tôi tại Tweag. Khi kiểm tra hợp đồng Plutus, chúng ta cần có khả năng hoạt động như một kẻ tấn công và sửa đổi các giao dịch để nghiên cứu cách những người xác thực sẽ phản ứng.

Bằng cách sử dụng trình xác thực đã nấu chín để phát triển mã ngoài chuỗi của bạn, bạn sẽ có thể kiểm tra nhiều thuộc tính an toàn và tính đúng đắn của mã trên chuỗi của bạn và điều này có thể làm tăng đáng kể sự tin tưởng của bạn vào tính đúng đắn của mã. Điều đó có thể tiết kiệm thời gian và tiền bạc trong quá trình kiểm tra. Trên thực tế, bước đầu tiên của quá trình kiểm tra Tweag là viết mã tạo giao dịch bằng cách sử dụng trình xác thực nấu chín, để sau đó có thể tương tác với cơ sở hạ tầng của khách hàng của chúng tôi một cách tự do.

Tổng hợp

Comments (No)

Leave a Reply