Безпека типів

Типобезпечність (англ. type safety) — властивість мови програмування, яка характеризує безпеку та надійність у застосуванні її системи типів.

Систему типів називають безпечною (англ. safe) або надійною (англ. sound), якщо у програмах, які пройшли перевірку узгодження типів (англ. well-typed programs або well-formed programs), виключено можливість виникнення помилок узгодження типів ^[en].

Помилка узгодження типів або помилка типізації (англ. type error) — неузгодженість типів компонентів виразів у програмі, наприклад спроба використати ціле число як функцію. Пропущені помилки узгодження типів на етапі виконання можуть спричиняти баги і навіть креші програм. Безпека мови не є синонімом повної відсутності багів, але щонайменше вони стають досліджуваними в рамках семантики мови (формальної або неформальної).

Надійні системи типів також називають сильними (англ. strong), але трактування цього терміна часто пом'якшують, крім того, його часто застосовують до мов, які здійснюють динамічну перевірку узгодження типів (сильна та слабка типізація).

Іноді безпечність розглядають як властивість конкретної програми, а не мови, якою її написано — тому що деякі типобезпечні мови дозволяють обійти або порушити систему типів, якщо програміст практикує мізерну типобезпеку. Поширена думка, що такі можливості на практиці є необхідними, але це вигадка. Поняття про «безпечність програми» є важливим у тому сенсі, що реалізація безпечної мови сама може бути небезпечною. Розкрутка компілятора вирішує цю проблему, забезпечуючи мові безпечність не лише в теорії, але й на практиці.

Подробиці

Робіну Мілнеру належить вираз «Програми, що пройшли перевірку типів, не можуть „збитися зі шляху істинного“». Тобто, безпечна система типів запобігає свідомо помилковим операціям, пов'язаним із хибними типами. Наприклад, вираз 8 / "Hello, World" очевидно є помилковим, оскільки арифметика не визначає операції ділення числа на рядок. Формально, безпечність означає гарантію того, що значення будь-якого виразу, який пройшов перевірку типів і має тип τ є істинним елементом множини значень τ, тобто лежатиме в межах діапазону значень, допустимого статичним типом цього виразу. Насправді, у цій вимозі є нюанси — див. ^[en] та складні випадки поліморфізму.

Крім того, інтенсивне використання механізмів визначення нових типів запобігає логічним помилкам, які походять із семантики різних типів. Наприклад, і міліметри, і дюйми є одиницями довжини і можуть бути подані цілими числами, але буде помилкою віднімати дюйми від міліметрів, і розвинена система типів не допустить цього (зрозуміло, за умови, що програміст використовує для значень, виражених у різних одиницях, різні типи даних, а не описує і ті, й інші як змінні цілого типу). Іншими словами, безпечність мови означає, що мова захищає програміста від його власних можливих помилок.

Багато мов системного програмування (наприклад, Ада, Сі, ) передбачають ненадійні (англ. unsound) або небезпечні (англ. unsafe) операції, призначені для можливості порушити (англ. violate) систему типів (див. Зведення типів і Каламбур типізації). В одних випадках це допускається лише в обмежених частинах програми, в інших — не відрізняється від добре типізованих операцій.

У мейнстримі^[] нерідко поняття типобезпеки звужують до «безпечності типів щодо доступу до пам'яті» (англ. memory type safety), що означає, що компоненти об'єктів одного агрегатного типу не можуть звертатися до комірок пам'яті, виділених під об'єкти іншого типу. Безпека доступу до пам'яті означає заборону можливості скопіювати довільний бітовий ланцюжок з однієї ділянки пам'яті в іншу. Наприклад, якщо мова передбачає тип t, що має обмежений спектр допустимих значень, і надає можливість скопіювати нетипізовані дані в змінну цього типу, то це не є типобезпечним, оскільки потенційно допускає, що змінна типу t матиме значення, яке не є допустимим для типу t. І, зокрема, якщо така небезпечна мова дозволяє записати довільне ціле значення в змінну, що має тип «вказівник», то небезпечність доступу до пам'яті очевидна (див. Завислі вказівники). Прикладами небезпечних мов є C і . У спільнотах цих мов часто називають «безпечними» будь-які операції, які безпосередньо не призводять до падіння програми. Безпека доступу до пам'яті також запобігає можливості переповнення буфера, наприклад, спроби запису великорозмірних об'єктів у комірки, виділені для об'єктів іншого типу меншого розміру.

Надійні статичні системи типів консервативні (надлишкові) в тому сенсі, що відкидають навіть програми, які виконалися б коректно. Причина цього полягає в тому, що для будь-якої тюрінг-повної мови, множина програм, які можуть породжувати помилки узгодження типів під час виконання, алгоритмічно нерозв'язна (див. Проблема зупинки). Як наслідок, такі системи типів забезпечують ступінь захисту, суттєво вищий, ніж це необхідно для забезпечення безпеки доступу до пам'яті. З іншого боку, безпечність деяких дій неможливо довести статично, її слід контролювати динамічно (наприклад, індексація масиву з довільним доступом). Такий контроль може здійснюватися або ^[en] самої мови, або безпосередньо функціями, що реалізують подібні потенційно небезпечні операції.

Сильно динамічно типізовані мови (наприклад, Лісп, Smalltalk) не допускають пошкодження даних завдяки тому, що програма, яка намагається перетворити значення до несумісного типу, породжує виняток. До переваг сильної динамічної типізації перед типобезпечністю можна віднести відсутність консервативності, як наслідок, розширення спектра розв'язуваних завдань програмування. Ціною цього стає неминуче зниження швидкодії програм, а також необхідність значно більшої кількості пробних запусків для виявлення можливих помилок. Тому багато мов комбінують у той чи інший спосіб можливості статичного та динамічного контролю узгодження типів.

Приклади безпечних мов

Ада

Ада (найбільш типобезпечна мова в сімействі Паскалю) орієнтована на розробку надійних вбудовуваних систем, драйверів та інші завдання системного програмування. Для реалізації критичних секцій Ада надає низку небезпечних конструкцій, імена яких зазвичай починаються з Unchecked_.

Мова SPARK є підмножиною Ади. З нього усунуто небезпечні можливості, але додано можливості проєктування за контрактом. SPARK виключає можливість виникнення завислих вказівників за допомогою виключення можливості динамічного виділення пам'яті. Статично перевірювані контракти додано до Ada2012.

Гоар у тюрінгівській лекції стверджував, що задля забезпечення надійності мало статичних перевірок — надійність насамперед є наслідком простоти . Тоді ж він передбачив, що складність Ади спричинить катастрофи.

BitC

 — гібридна мова, що комбінує низькорівневі можливості Сі з безпекою Standard ML та лаконічністю Scheme. BitC орієнтована на розробку надійних вбудовуваних систем, драйверів та вирішення інших завдань системного програмування.

Cyclone

Дослідницька мова Cyclone є безпечним діалектом мови C, що запозичує багато ідей з ML (зокрема, типобезпечний ). Призначена для тих самих завдань, що й C, і після здійснення всіх перевірок компілятор породжує код на ANSI C. Не потребує для забезпечення динамічної безпеки віртуальної машини або збирання сміття — натомість заснована на ^[en]. Cyclone встановлює вищу планку вимог безпеки сирцевого коду, і через небезпечність природи C портування навіть простих програм із C на Cyclone може вимагати певної роботи, хоча чималу її частину можна проробити в рамках C до зміни компілятора. Тому Cyclone часто визначають не як діалект C, а як «мову, синтаксично і семантично схожу на C».

Rust

Багато ідей Cyclone втілено в мові Rust. Крім сильної статичної типізації у мову додано статичний аналіз часу життя вказівників, заснований на концепції «володіння». Реалізовано статичні обмеження, що блокують потенційно некоректний доступ до пам'яті: відсутні нульові вказівники, неможлива поява неініціалізованих та деініціалізованих змінних, заборонено спільне використання змінюваних змінних кількома завданнями. Перевірка на вихід за межі масиву є обов'язковою.

Haskell

Haskell (нащадок ML) спочатку розроблявся як мова, що мало зробити поведінку програм нею ще більш передбачуваною, ніж ранніми діалектами ML. Однак, пізніше до стандарту мови додано небезпечні операції, необхідні у повсякденній практиці, хоча й позначені відповідними ідентифікаторами (починаються з unsafe).

Haskell також надає можливості слабкої динамічної типізації, і до стандарту мови включено реалізацію механізму обробки винятків за допомогою цих можливостей. Її використання може призводити до аварійного завершення програм, за що ^[en] назвав Haskell виключно небезпечним. Він вважає неприйнятним той факт, що винятки мають тип, визначений користувачем у контексті класу типів Typeable, з урахуванням того, що винятки генерує безпечний код (за межами IO); і класифікує повідомлення про внутрішню помилку, яке видає компілятор, як невідповідне гаслу Мілнера. В обговоренні показано, як можна було б реалізувати в Haskell'і статично типобезпечні винятки в стилі Standard ML.

Лісп

«Чистий» (мінімальний) Лісп є однотиповою мовою (тобто будь-яка конструкція належить до типу «S-вираз»), хоча навіть перші промислові реалізації Lisp передбачали принаймні певну кількість ^[en]. Сімейство нащадків мови Lisp утворюють переважно динамічно типізовані мови, але існують статично типізовані і такі, що поєднують обидві форми типізації.

Common Lisp є сильно динамічно типізованою мовою, але передбачає можливість явно (^[en]) призначати типи (а компілятор SBCL здатний сам їх виводити), однак, ця можливість використовується для оптимізації та посилення динамічних перевірок і не означає статичної типобезпеки. Програміст, з метою підвищення швидкодії, може встановити для компілятора знижений рівень динамічних перевірок, і тоді скомпільовану програму вже не можна вважати безпечною.

Мова Scheme також є динамічно типізованою мовою, але компілятор ^[en] статично виводить типи, використовуючи їх для агресивної оптимізації програм. Мови «Typed Racket» (розширення Racket Scheme) і типобезпечні. Clojure поєднує сильний динамічний та статичний контроль типів.

ML

Спочатку мова ML розроблялася як інтерактивна система доведення теорем, і лише згодом стала самостійною компільованою мовою загального призначення. Багато зусиль було приділено доведенню надійності системі типів Гіндлі — Мілнера, що лежить в основі ML. Доведення надійності побудовано для підмножини («Fuctional ML»), розширення посилальними типами («Reference ML»), розширення винятками («Exception ML»), для мови, що об'єднує всі ці розширення («Core ML») і нарешті, його розширення першокласними продовженнями («Control ML»), спершу мономорфними, потім поліморфними.

Наслідком цього стало те, що нащадки ML найчастіше апріорі вважаються типобезпечними, навіть попри, що деякі з них відкладають значущі перевірки на програми (OCaml), або відхиляються від семантики, для якої побудовано доведення надійності, і містять небезпечні можливості явно (Haskell). Мовам сімейства ML характерна розвинена підтримка алгебричних типів даних, використання яких суттєво сприяє запобіганню логічних помилок, що також підтримує враження типобезпеки.

Деякі нащадки ML також є інструментами інтерактивного доведення (^[en], ^[en], Agda). Багато хто з них, хоча й могли б використовуватися для безпосередньої розробки програм із доведеною надійністю, частіше використовуються для верифікації програм іншими мовами — з таких причин, як висока трудомісткість використання, низька швидкодія, відсутність ^[en] тощо. Серед нащадків ML із доведеною надійністю виділяються як орієнтовані на промислове застосування мови Standard ML і прототип його подальшого розвитку successor ML (раніше відома як «ML2000»).

Standard ML

Мова Standard ML (старша в сімействі мов ML) орієнтована на розробку ^[en] програм промислової швидкодії. Мова має строге формальне визначення та доведену статичну та динамічну безпечність. Після статичної перевірки узгодженості інтерфейсів компонентів програми (зокрема, породжуваних — див. ^[ru]), подальший контроль безпеки підтримується -системою. Як наслідок, навіть програма, що містить помилку, на Standard ML завжди продовжує поводитися як ML-програма: вона може надовго піти в обчислення або видати користувачеві повідомлення про помилку, але вона не може впасти.

Однак деякі реалізації (^[en], Mythryl, ^[en]) включають нестандартні бібліотеки, що надають певні небезпечні операції (їх ідентифікатори починаються з Unsafe). Ці можливості необхідні для ^[en] цих реалізацій, що забезпечує взаємодію з не-ML-кодом (зазвичай це код на C що реалізує критичні за швидкістю компоненти програм), який може вимагати своєрідного бітового подання даних. Крім того, багато реалізацій Standard ML, хоча самі написані на ньому самому, використовують рантайм-систему, написану на C. Іншим прикладом є режим REPL компілятора SML/NJ, який використовує небезпечні операції виконання інтерактивно введеного програмістом коду.

Мова Alice, розширення Standard ML, надає можливості сильної динамічної типізації.

Див. також

• ^[en]
• Креш
• Теорія типів
• Формальна верифікація
• Автоматичне доведення теорем
• Приведення типів
• Каламбур типізації

Примітки

1. Ахо-Сети-Ульман та 1985, 2001, 2003, с. 340, Статическая и динамическая проверка типов.
2. Wright, Felleisen, 1992.
3. Cardelli - Typeful programming, 1991, с. 3.
4. Mitchel - Concepts in Programming Languages, 2004, с. 132—133, 6.2.1 Type Safety.
5. Java is not type-safe.
6. Harper, 2012, с. 35, Chapter 4. Statics.
7. Mitchel - Concepts in Programming Languages, 2004, с. 130, 6.1.2 Type Errors.
8. Appel - A Critique of Standard ML, 1992, с. 2, Safety.
9. Paulson, 1996, с. 2.
10. Milner - A Theory of Type Polymorphism in Programming, 1978.
11. Cardelli - Typeful programming, 1991, с. 51, 9.3. Type violations.
12. Mitchel - Concepts in Programming Languages, 2004, с. 133—135, 6.2.2 Compile-Time and Run-Time Checking.
13. Pierce, 2002, с. 3, 1.1 Типы в информатике.
14. Cardelli - Typeful programming, 1991, с. 49, 9.1 Dynamic types.
15. C.A.R. Hoare — The Emperor's Old Clothes, Communications of the ACM, 1981
16. unsafeCoerce Архівна копія на сайті Wayback Machine. (мова Haskell)
17. System.IO.Unsafe Архівна копія на сайті Wayback Machine. (мова Haskell)
18. Haskell Is Exceptionally Unsafe.
19. Cardelli, Wegner - On Understanding Types, 1985, с. 3, 1.1. Organizing Untyped Universes.
20. Common Lisp HyperSpec. оригіналу за 16 червня 2013. Процитовано 26 травня 2013.
21. SBCL Manual — Declarations as Assertions. оригіналу за 20 січня 2015. Процитовано 20 січня 2015.
22. . Архів оригіналу за 7 січня 2009. Процитовано 23 грудня 2014.
23. Appel - A Critique of Standard ML, 1992.
24. Robin Milner, Mads Tofte. Commentary on Standard ML. — Universiry of Edinburg, University of Nigeria, 1991. — 7 липня. з джерела 1 грудня 2014.

Література

• Robin Milner. A Theory of Type Polymorphism in Programming. — Jcss, 1978. — Vol. 17 (7 July). — P. 348—375.
• Stavros Macrakis. Safety and power // ACM SIGSOFT Software Engineering Notes. — 1982. — Vol. 7, iss. 2, no. April (7 July). — P. 25—26. — DOI:10.1145/1005937.1005941.
• Luca Cardelli, Peter Wegner. On Understanding Types, Data Abstraction, and Polymorphism. — , 1985. — 7 July. — P. 471—523. — ISSN 0360-0300.
• Альфред Ахо, Рави Сети, Джеффри Ульман. Компиляторы: принципы, технологии и инструменты. — Addison-Wesley Publishing Company, Издательский дом «Вильямс», 1985, 2001, 2003. — 768 с. — (рус.), 0-201-10088-6 (ориг.).
• ^[en]. Typeful programming // IFIP State-of-the-Art Reports. — Springer-Verlag, 1991. — Iss. Formal Description of Programming Concepts (7 July). — P. 431—507.
• Andrew W. Appel. A Critique of Standard ML. — Princeton University, revised version of CS-TR-364-92, 1992. — 7 July.
• Andrew K. Wright, ^[en]. A Syntactic Approach to Type Soundness // Information and Computation. — 1992. — Vol. 115, iss. 1 (7 July). — P. 38—94. — DOI:10.1006/inco.1994.1093.
• Lawrence C. Paulson. ML for the Working Programmer. — 2nd. — Cambridge University Press, 1996. — 492 с. — (тверда обкладинка), 0-521-56543-X (м'яка обкладинка).
• Pierce, Benjamin C. Types and Programming Languages. — MIT Press, 2002. — .
• John C. Mitchell. Concepts in Programming Languages. — Cambridge University Press, 2004. — (електронна книга в netLibrary); 0-521-78098-5 (тверда обкладинка).
• Harper. . — version 1.37 (revised 01.11.2014). — licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 United States License, 2012. — 544 с. Архівовано жовтень 24, 2015 на сайті Wayback Machine.
• Vijay Saraswat. Java is not type-safe.

Посилання

• Type Safe. Portland Pattern Repository Wiki. Процитовано 5 лютого 2014.
• . Haskell Is Exceptionally Unsafe.