EverCrypt: კრიპტოგრაფიული ვერიფიკაციის ბიბლიოთეკა

ევერესტის პროექტი

მკვლევარები ინფორმატიკისა და ავტომატიზაციის კვლევის სახელმწიფო ინსტიტუტი (ინრია), Microsoft Research– მა და კარნეგი მელონის უნივერსიტეტმა წარმოადგინეს პირველი საცდელი გამოცემა EverCrypt კრიპტო ბიბლიოთეკა შემუშავდა ევერესტის პროექტის ფარგლებში და ფორმალური საიმედოობის შემოწმების მათემატიკური მეთოდების გამოყენებით.

თავისი შესაძლებლობებისა და მუშაობისთვის, EverCrypt ძალიან ახლოს არის არსებულ კრიპტო ბიბლიოთეკებთან (OpenSSL), მაგრამ ეს, მათგან განსხვავებით, გთავაზობთ საიმედოობისა და უსაფრთხოების დამატებით გარანტიებს.

მაგალითად გადამოწმების პროცესი იწურება დეტალური სპეციფიკაციების განსაზღვრამდე რომ აღწერს პროგრამის ყველა ქცევას და მათემატიკური მტკიცებულება, რომ წერილობითი კოდი აკმაყოფილებს მომზადებულ სპეციფიკაციებს.

მტკიცებულებებზე დაფუძნებული ხარისხის კონტროლის მეთოდებისგან განსხვავებით, გადამოწმება უზრუნველყოფს საიმედო გარანტიებს რომ პროგრამა იმუშავებს მხოლოდ ისე როგორც დეველოპერები აპირებდნენ და არ არსებობს რაიმე სახის შეცდომები.

მაგალითად, სპეციფიკაციის შესაბამისობა უზრუნველყოფს მეხსიერებასთან უსაფრთხო მუშაობას და შეცდომების არარსებობას, რაც ბუფერული გადახურვას იწვევს, მითითების მითითებისკენ, უკვე გათავისუფლებული მეხსიერების არეებზე შესასვლელად ან მეხსიერების ბლოკების ორმაგად გათავისუფლება.

რა არის EverCrypt?

EverCrypt უზრუნველყოფს ძლიერი ტიპისა და მნიშვნელობის შემოწმებას- კომპონენტი არასოდეს გადასცემს პარამეტრებს სხვა შეუსაბამო კომპონენტთან და ვერ მიიღებს წვდომას სხვა კომპონენტების შიდა მდგომარეობებზე.

შეყვანის / გამოყვანის ქცევა სრულად შეესაბამება მათემატიკის ფუნქციის მარტივ მოქმედებებს, რომლებიც განსაზღვრულია კრიპტოგრაფიულ სტანდარტებში.

თავდასხმებისგან დასაცავად მესამე მხარის არხებში, გამოთვლების დროს ქცევა (მაგალითად, შესრულების ხანგრძლივობა ან გარკვეულ მეხსიერებაზე წვდომის არსებობა) ეს არ არის დამოკიდებული საიდუმლო მონაცემებზე, რომელიც დამუშავებულია.

პროექტის კოდი იწერება ფუნქციურ ენაზე F * (F ვარსკვლავი) , რომელიც უზრუნველყოფს დამოკიდებული ტიპების და დახვეწის სისტემასპროგრამების ზუსტი სპეციფიკაციების (მათემატიკური მოდელის) დადგენისა და SMT ფორმულების და დამხმარე ტესტის საშუალებებით სისწორისა და შეცდომების არარსებობის გარანტია.

F * ში კოდი ვრცელდება Apache 2.0 ლიცენზიით, ხოლო საბოლოო მოდულები C და ასამბლეაში MIT ლიცენზიით.

მითითების კოდის საფუძველზე F *, წარმოიქმნება assembler, C, OCaml, JavaScript და ვებ ასამბლეის კოდი.

კოდის ზოგიერთი ნაწილი მომზადებული პროექტი უკვე გამოიყენება Firefox– ში, Windows– ის ბირთვში , ბლოკჩეინი Tezos და VPN Wireguard.

EverCrypt კომპონენტები

Იდეაში, EverCrypt აერთიანებს ორ ადრე განსხვავებულ პროექტს HACL * და Vale– სგან, მათზე დაფუძნებული ერთიანი API- ს უზრუნველყოფა და რეალური პროექტების გამოყენებისთვის შესაფერისი.

HACL * დაწერილია Low* და მისი მიზანია უზრუნველყოს კრიპტოგრაფიული პრიმიტივების გამოყენება C პროგრამებში ისინი იყენებენ libsodium და NaCL სტილის API- ს.

პროექტი ვალემ შეიმუშავა სპეციფიკური ენა დომენის ასამბლეაში გადამოწმების შესაქმნელად.

კომბინირებულია დაახლოებით 110 ათასი ხაზი HACL * კოდი დაბალ * ენაზე და 25 ათასი ხაზი კოდი Val– ისთვის და ისინი გადაწერილია 70 ათას კოდექსში უნივერსალურ ენაზე F *, რომელიც ასევე მუშავდება ევერესტის პროექტის ფარგლებში.

EverCrypt ბიბლიოთეკის პირველი ვერსია შემოწმებულია შესრულებები შემდეგი კრიპტოგრაფიული ალგორითმების შემოთავაზებულია C ან ასამბლეის ვერსიებში (როდესაც იყენებთ.

პროექტის შემდეგ გამოირჩევა შემდეგიდან:

  • ჰეშის ალგორითმები: SHA2, SHA3, SHA1 და MD5 ყველა ვარიანტი
  • ავთენტიფიკაციის კოდები: HMAC მეტი SHA1, SHA2-256, SHA2-384 და SHA2-512 მონაცემთა წყაროს ავთენტიფიკაციისთვის
  • HKDF გასაღების გენერაციის ალგორითმი (HMAC დაფუძნებული ამონაწერი და გაფართოება ძირითადი წარმოების ფუნქცია)
  • ChaCha20 ნაკადის დაშიფვრა (ხელმისაწვდომია არაოპტიმიზირებული C ვერსია)
  • Poly1305 შეტყობინებების ავთენტიფიკაციის ალგორითმი (MAC) (C და ასამბლეის ვერსია)
  • Diffie-Hellman პროტოკოლი ელიფსური მრუდის მრუდის შესახებ 25519
  • დაბლოკვის შიფრირების რეჟიმი AEAD (ავთენტიფიცირებული შიფრი) ChachaPoly (ვერსია C არ არის ოპტიმიზირებული)
  • AEAD AES-GCM ბლოკის დაშიფვრის რეჟიმი (ასამბლეის ვერსია AES-NI ოპტიმიზაციებით).

Პირველად ალფა ვერსია, კოდის გადამოწმება უკვე დასრულებულია მეტწილად, მაგრამ ჯერ კიდევ არის აღმოფხვრილი რამდენიმე რაიონი.

გარდა ამისა, API ჯერ არ არის სტაბილიზებული, რომელიც გაფართოვდება შემდეგ ალფა ვერსიებში (დაგეგმილია სტრუქტურების გაერთიანება ყველა API- სთვის.

ხარვეზებს შორის ხაზგასმულია x86_64 არქიტექტურასთან შესაბამისობა (პირველ ეტაპზე, მთავარი მიზანი არის საიმედოობა, ხოლო ოპტიმიზაცია და პლატფორმები განხორციელდება მეორე ადგილზე).

წყარო: https://jonathan.protzenko.fr


სტატიის შინაარსი იცავს ჩვენს პრინციპებს სარედაქციო ეთიკა. შეცდომის შესატყობინებლად დააჭირეთ ღილაკს აქ.

იყავი პირველი კომენტარი

დატოვე კომენტარი

თქვენი ელფოსტის მისამართი გამოქვეყნებული არ იყო. აუცილებელი ველები აღნიშნულია *

*

*

  1. მონაცემებზე პასუხისმგებელი: მიგელ ანგელ გატონი
  2. მონაცემთა მიზანი: სპამის კონტროლი, კომენტარების მართვა.
  3. ლეგიტიმაცია: თქვენი თანხმობა
  4. მონაცემთა კომუნიკაცია: მონაცემები არ გადაეცემა მესამე პირებს, გარდა სამართლებრივი ვალდებულებისა.
  5. მონაცემთა შენახვა: მონაცემთა ბაზა, რომელსაც უმასპინძლა Occentus Networks (EU)
  6. უფლებები: ნებისმიერ დროს შეგიძლიათ შეზღუდოთ, აღადგინოთ და წაშალოთ თქვენი ინფორმაცია.