Тип безопасности

В информатике язык безопасность типов и правильность типов — это степень, в которой программирования препятствует или предотвращает ошибки типов . Типовую безопасность иногда альтернативно считают свойством средств компьютерного языка; то есть некоторые средства типобезопасны, и их использование не приведет к ошибкам типа, в то время как другие средства на том же языке могут быть небезопасными по типу, и использующая их программа может столкнуться с ошибками типа. Поведения, классифицируемые как ошибки типа в данном языке программирования, обычно являются результатом попыток выполнить операции со значениями , которые не относятся к соответствующему типу данных , например, добавление строки к целому числу , когда нет определения, как обрабатывать этот случай. . Эта классификация частично основана на мнениях.

Обеспечение соблюдения типов может быть статическим, выявляющим потенциальные ошибки во время компиляции , или динамическим, когда информация о типе связывается со значениями во время выполнения и анализируется по мере необходимости для обнаружения неизбежных ошибок, или комбинация того и другого. Применение динамического типа часто позволяет запускать программы, которые были бы недействительны при статическом применении.

В контексте статических систем типов (время компиляции) безопасность типов обычно включает (помимо прочего) гарантию того, что конечное значение любого выражения будет законным членом статического типа этого выражения. Точное требование более тонкое — см., например, подтипирование и полиморфизм для осложнений.

Определения

Интуитивно, правильность шрифта отражается в Робина Милнера содержательном заявлении о том, что

Хорошо типизированные программы не могут «пойти не так».

Другими словами, если система типов является правильной , то выражения, принятые этой системой типов, должны оцениваться как значение соответствующего типа (а не создавать значение какого-либо другого, несвязанного типа или аварийно завершать работу с ошибкой типа). Виджай Сарасват дает следующее связанное определение:

Язык является типобезопасным, если с данными на нем можно выполнять только те операции, которые разрешены типом данных.

Однако то, что именно означает, что программа «хорошо типизирована» или «работает неправильно», — это свойства ее статической и динамической семантики , которые специфичны для каждого языка программирования. Следовательно, точное формальное определение правильности типов зависит от стиля формальной семантики, используемой для определения языка. В 1994 году Эндрю Райт и Маттиас Феллизен сформулировали то, что стало стандартным методом определения и доказательства безопасности типов в языках, определяемых операционной семантикой : что наиболее близко к понятию типовой безопасности, как оно понимается большинством программистов. Согласно этому подходу, семантика языка должна обладать следующими двумя свойствами, чтобы считаться типозвуком:

Прогресс

Правильно типизированная программа никогда не «застревает»: каждое выражение либо уже является значением , либо может быть уменьшено до значения каким-то четко определенным способом. Другими словами, программа никогда не попадает в неопределенное состояние, в котором дальнейшие переходы невозможны.

Сохранение (или предметное сокращение )

После каждого шага вычисления тип каждого выражения остаётся прежним (то есть сохраняется его тип ) .

Ряд других формальных трактовок правильности типов также был опубликован с точки зрения денотационной семантики и структурной операционной семантики .

Связь с другими формами безопасности

В отдельности надежность типов является относительно слабым свойством, поскольку, по сути, она просто утверждает, что правила системы типов внутренне непротиворечивы и не могут быть нарушены. Однако на практике языки программирования устроены таким образом, что правильная типизация также влечет за собой и другие, более сильные свойства, некоторые из которых включают:

• Предотвращение незаконных операций. Например, система типов может отклонить выражение 3 / "Hello, World" деления оператор не определен строки как недействительный, поскольку для делителя .
• Безопасность памяти
  • Системы типов могут предотвратить появление диких указателей , которые в противном случае могли бы возникнуть из-за того, что указатель на один тип объекта обрабатывается как указатель на другой тип.
  • Более сложные системы типов, например те, которые поддерживают зависимые типы , могут обнаруживать и отклонять внешний доступ, предотвращая потенциальное переполнение буфера .
• Логические ошибки, возникающие в семантике разных типов. Например, дюймы и миллиметры могут храниться как целые числа, но их не следует заменять или складывать. Система типов может обеспечить для них два разных типа целых чисел.

Типобезопасные и типобезопасные языки.

Безопасность типов обычно является требованием для любого игрушечного языка (т. е. эзотерического языка ), предлагаемого в академических исследованиях языков программирования. С другой стороны, многие языки слишком велики для доказательств безопасности типов, генерируемых человеком, поскольку они часто требуют проверки тысяч случаев. Тем не менее, было доказано, что некоторые языки, такие как Standard ML , который имеет строго определенную семантику, соответствуют одному определению типовой безопасности. некоторые другие языки, такие как Haskell Считается , что чтобы соответствовать некоторому определению безопасности типов, при условии, что не используются определенные функции «экранирования» (например, Haskell unsafePerformIO , используемый для «выхода» из обычной ограниченной среды, в которой возможен ввод-вывод, обходит систему типов и поэтому может использоваться для нарушения безопасности типов. ) Каламбур — еще один пример такой функции «побега». Независимо от свойств определения языка, определенные ошибки могут возникать во время выполнения из-за ошибок в реализации или в связанных библиотеках, написанных на других языках; такие ошибки могут сделать данный тип реализации небезопасным в определенных обстоятельствах. Ранняя версия виртуальной машины Sun Java была уязвима для подобных проблем.

Сильная и слабая типизация

Основная статья: Сильная и слабая типизация

Языки программирования часто в разговорной речи классифицируются как строго типизированные или слабо типизированные (также слабо типизированные), чтобы указать на определенные аспекты безопасности типов. В 1974 году Лисков и Зиллес определили строго типизированный язык как язык, в котором «всякий раз, когда объект передается от вызывающей функции к вызываемой функции, его тип должен быть совместим с типом, объявленным в вызываемой функции». В 1977 году Джексон писал: «В строго типизированном языке каждая область данных будет иметь отдельный тип, и каждый процесс будет формулировать свои требования к коммуникации в терминах этих типов». Напротив, слабо типизированный язык может давать непредсказуемые результаты или выполнять неявное преобразование типов.

Управление памятью и безопасность типов

Безопасность типов тесно связана с безопасностью памяти . Например, в реализации языка, имеющего некоторый тип $t$ который допускает некоторые битовые шаблоны, но не другие, ошибка висячего указателя памяти позволяет записать битовый шаблон, который не представляет законный член $t$ в мертвую переменную типа $t$, вызывая ошибку типа при чтении переменной. И наоборот, если язык безопасен для памяти, он не может позволить использовать произвольное целое число в качестве указателя , следовательно, должен быть отдельный указатель или ссылочный тип.

В качестве минимального условия типобезопасный язык не должен допускать висячих указателей в выделениях разных типов. Но большинство языков требуют правильного использования абстрактных типов данных , определенных программистами, даже если это не является строго необходимым для безопасности памяти или предотвращения каких-либо катастрофических сбоев. Выделениям присваивается тип, описывающий их содержимое, и этот тип фиксируется на время выделения. на основе типов Это позволяет анализу псевдонимов сделать вывод о том, что выделения разных типов различны.

Большинство типизированных языков используют сборку мусора . Пирс говорит: «чрезвычайно сложно добиться безопасности типов при наличии явной операции освобождения» из-за проблемы висячего указателя. Однако Rust обычно считается типобезопасным и для обеспечения безопасности памяти использует проверку заимствований вместо сборки мусора.

Безопасность типов в объектно-ориентированных языках

В объектно-ориентированных языках безопасность типов обычно обусловлена ​​наличием типов системы . Это выражается в определениях классов.

Класс . по существу определяет структуру производных от него объектов и API как контракт для обработки этих объектов Каждый раз, когда создается новый объект, он будет соответствовать этому контракту.

Каждая функция, которая обменивает объекты, производные от определенного класса или реализующие определенный интерфейс , будет придерживаться этого контракта: следовательно, в этой функции разрешены только операции с этим объектом, определенные методами класса, который реализует объект. Это будет гарантией сохранения целостности объекта.

Исключением являются объектно-ориентированные языки, которые допускают динамическое изменение структуры объекта или использование отражения для изменения содержимого объекта для преодоления ограничений, налагаемых определениями методов класса.

Проблемы безопасности ввода на определенных языках

Есть

Ada была разработана так, чтобы подходить для встроенных систем , драйверов устройств и других форм системного программирования , а также для поощрения типобезопасного программирования. Чтобы разрешить эти противоречивые цели, Ада ограничивает небезопасность типов определенным набором специальных конструкций, имена которых обычно начинаются со строки Не отмечено_ . Unchecked_Deallocation можно эффективно запретить в блоке текста Ada, применив прагма Чистая к этому агрегату. Ожидается, что программисты будут использовать Unchecked_ строит очень осторожно и только при необходимости; программы, которые их не используют, являются типобезопасными.

Язык программирования SPARK — это подмножество Ada, устраняющее все его потенциальные двусмысленности и ненадежности и в то же время добавляющее статически проверяемые контракты к доступным функциям языка. SPARK позволяет избежать проблем с висячими указателями , полностью запрещая выделение во время выполнения.

Ada2012 добавляет в сам язык статически проверяемые контракты (в виде пред- и постусловий, а также инвариантов типов).

С

Язык программирования C типобезопасен в ограниченном контексте; например, ошибка времени компиляции генерируется при попытке преобразовать указатель на структуру одного типа в указатель на структуру другого типа, если только не используется явное приведение. Однако ряд очень распространенных операций не являются типобезопасными; например, обычный способ печати целого числа — это что-то вроде printf("%d", 12), где %d рассказывает printf во время выполнения ожидать целочисленный аргумент. (Что-то вроде printf("%s", 12), который сообщает функции ожидать указатель на символьную строку и при этом предоставляет целочисленный аргумент, может быть принят компиляторами, но приведет к неопределенным результатам.) Это частично смягчается некоторыми компиляторами (такими как gcc), проверяющими соответствие типов между аргументы printf и строки формата.

Кроме того, C, как и Ada, обеспечивает неопределенные или неопределенные явные преобразования; и, в отличие от Ada, идиомы, использующие эти преобразования, очень распространены и помогли создать C репутацию небезопасного типа. Например, стандартный способ выделения памяти в куче — вызвать функцию выделения памяти, например malloc, с аргументом, указывающим, сколько байт требуется. Функция возвращает нетипизированный указатель (типа void *), который вызывающий код должен явно или неявно привести к соответствующему типу указателя. Предварительно стандартизированные реализации C требовали явного приведения типов, поэтому код (struct foo *) malloc(sizeof(struct foo)) стало общепринятой практикой.

С++

Некоторые особенности C++, способствующие созданию более типобезопасного кода:

• Оператор new возвращает указатель типа, основанного на операнде, тогда как malloc возвращает указатель void.
• Код C++ может использовать виртуальные функции и шаблоны для достижения полиморфизма без указателей void.
• Более безопасные операторы приведения, такие как динамическое приведение , выполняющее проверку типов во время выполнения.
• Строго типизированные перечисления C++11 не могут быть неявно преобразованы в целые числа или другие типы перечислений или из них.
• Явные конструкторы C++ и операторы явного преобразования C++11 предотвращают неявные преобразования типов.

С#

C# является типобезопасным. Он поддерживает нетипизированные указатели, но доступ к ним должен осуществляться с использованием ключевого слова «unsafe», которое можно запретить на уровне компилятора. Он имеет встроенную поддержку проверки приведения типов во время выполнения. Приведения можно проверить с помощью ключевого слова «as», которое вернет нулевую ссылку, если приведение недопустимо, или с помощью приведения в стиле C, которое выдаст исключение, если приведение недействительно. См. операторы преобразования C Sharp .

Неоправданная зависимость от типа объекта (от которого произошли все остальные типы) рискует противоречить цели системы типов C#. Обычно лучше отказаться от ссылок на объекты в пользу дженериков , подобных шаблонам в C++ и дженерикам в Java .

Ява

Язык Java предназначен для обеспечения безопасности типов. Все в Java происходит внутри объекта. и каждый объект является экземпляром класса .

Чтобы реализовать обеспечение безопасности типов , каждый объект перед использованием должен быть выделен . Java позволяет использовать примитивные типы , но только внутри правильно выделенных объектов.

Иногда часть безопасности типов реализуется косвенно: например, класс BigDecimal представляет число с плавающей запятой произвольной точности, но обрабатывает только числа, которые можно выразить с помощью конечного представления. Операция BigDecimal.divide() вычисляет новый объект как деление двух чисел, выраженных как BigDecimal.

В этом случае, если деление не имеет конечного представления, как при вычислении, например, 1/3=0,33333..., метод dive() может вызвать исключение, если для операции не определен режим округления. Следовательно, библиотека, а не язык, гарантирует, что объект соблюдает контракт, заложенный в определении класса.

Стандартный ML

Стандартный ML имеет строго определенную семантику и известен как типобезопасный. Однако некоторые реализации, включая Standard ML of New Jersey (SML/NJ), его синтаксический вариант Mythryl и MLton , предоставляют библиотеки, которые предлагают небезопасные операции. Эти средства часто используются вместе с интерфейсами внешних функций этих реализаций для взаимодействия с кодом, отличным от ML (например, с библиотеками C), для которого могут потребоваться данные, расположенные определенным образом. SML/NJ Другим примером является сам интерактивный верхний уровень , который должен использовать небезопасные операции для выполнения кода ML, введенного пользователем.

Модуль-2

Modula-2 — это строго типизированный язык, философия проектирования которого требует, чтобы любые небезопасные средства были явно помечены как небезопасные. Это достигается путем «перемещения» таких средств во встроенную псевдобиблиотеку под названием СИСТЕМА, откуда их необходимо импортировать, прежде чем их можно будет использовать. Таким образом, импорт делает видимым использование таких средств. К сожалению, это не было реализовано в исходном языковом отчете и его реализации. Все еще оставались небезопасные средства, такие как синтаксис приведения типов и варианты записей (унаследованные от Паскаля), которые можно было использовать без предварительного импорта. Трудность при перемещении этих средств в псевдомодуль СИСТЕМА заключалась в отсутствии какого-либо идентификатора средства, который затем можно было бы импортировать, поскольку можно импортировать только идентификаторы, но не синтаксис.

IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *)
VAR word : SYSTEM.WORD; addr : SYSTEM.ADDRESS;
addr := SYSTEM.ADR(word);

(* but type cast syntax can be used without such import *)
VAR i : INTEGER; n : CARDINAL;
n := CARDINAL(i); (* or *) i := INTEGER(n);

Стандарт ISO Modula-2 исправил это для возможности приведения типов, изменив синтаксис приведения типов на функцию под названием CAST, которую необходимо импортировать из псевдомодуля SYSTEM. Однако другие небезопасные возможности, такие как варианты записей, оставались доступными без какого-либо импорта из псевдомодуля СИСТЕМА.

IMPORT SYSTEM;
VAR i : INTEGER; n : CARDINAL;
i := SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)

Недавняя версия языка строго применяла исходную философию дизайна. Во-первых, псевдомодуль СИСТЕМА был переименован в НЕБЕЗОПАСНЫЙ, чтобы сделать небезопасный характер импортируемых оттуда объектов более явным. Затем все оставшиеся небезопасные объекты либо удалялись вообще (например, вариантные записи), либо переносились в псевдомодуль UNSAFE. Для объектов, где нет идентификатора, который можно было бы импортировать, были введены разрешающие идентификаторы. Чтобы включить такую ​​возможность, соответствующий идентификатор включения должен быть импортирован из псевдомодуля UNSAFE. В языке не осталось небезопасных объектов, не требующих импорта из UNSAFE.

IMPORT UNSAFE;
VAR i : INTEGER; n : CARDINAL;
i := UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *)

FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *)
<*FFI="C"*> (* pragma for foreign function interface to C *)

Паскаль

В Паскале имеется ряд требований к безопасности типов, некоторые из которых сохраняются в некоторых компиляторах. Если компилятор Паскаля требует «строгой типизации», две переменные не могут быть присвоены друг другу, если они не совместимы (например, преобразование целого числа в вещественное) или не присвоены идентичному подтипу. Например, если у вас есть следующий фрагмент кода:

type
  TwoTypes = record
     I: Integer;
     Q: Real;
  end;

  DualTypes = record
    I: Integer;
    Q: Real;
  end;

var
  T1, T2:  TwoTypes;
  D1, D2:  DualTypes;

При строгой типизации переменная, определяемая как TwoTypes не совместим с DualTypes (поскольку они не идентичны, даже если компоненты этого определяемого пользователем типа идентичны) и присвоение T1 := D2; является незаконным. Назначение T1 := T2; было бы законно, поскольку подтипы, для которых они определены, идентичны . Однако такое задание, как T1.Q := D1.Q; было бы законно.

Общий Лисп

В целом Common Lisp — типобезопасный язык. Компилятор Common Lisp отвечает за вставку динамических проверок для операций, типобезопасность которых не может быть доказана статически. Однако программист может указать, что программу следует скомпилировать с более низким уровнем динамической проверки типов. Программа, скомпилированная в таком режиме, не может считаться типобезопасной.

Примеры С++

Следующие примеры иллюстрируют, как операторы приведения C++ могут нарушить безопасность типов при неправильном использовании. Первый пример показывает, как могут быть неправильно преобразованы базовые типы данных:

#include <iostream>
using namespace std;

int main () {
    int   ival = 5;                              // integer value
    float fval = reinterpret_cast<float&>(ival); // reinterpret bit pattern
    cout << fval << endl;                        // output integer as float
    return 0;
}

В этом примере reinterpret_cast явно запрещает компилятору выполнять безопасное преобразование целого числа в значение с плавающей запятой. Когда программа запустится, она выведет мусорное значение с плавающей запятой. Проблему можно было бы избежать, написав вместо этого float fval = ival;

В следующем примере показано, как ссылки на объекты могут быть неправильно преобразованы вниз:

#include <iostream>
using namespace std;

class Parent {
public:
    virtual ~Parent() {} // virtual destructor for RTTI
};

class Child1 : public Parent {
public:
    int a;
};

class Child2 : public Parent {
public:
    float b;
};

int main () {
    Child1 c1;
    c1.a = 5;
    Parent & p = c1;                     // upcast always safe
    Child2 & c2 = static_cast<Child2&>(p); // invalid downcast
    cout << c2.b << endl;          // will output garbage data
    return 0;
}

Два дочерних класса имеют члены разных типов. При преобразовании указателя родительского класса на указатель дочернего класса результирующий указатель может не указывать на допустимый объект правильного типа. В примере это приводит к печати мусорного значения. Проблемы можно было избежать, заменив static_cast с dynamic_cast это вызывает исключение при недопустимых приведениях.

См. также

• Теория типов

Ссылки

• Пирс, Бенджамин К. (2002). Типы и языки программирования . МТИ Пресс. ISBN  978-0-262-16209-8 .
• «Тип сейф» . Вики-репозиторий портлендских шаблонов .
• Райт, Эндрю К.; Матиас Феллейзен (1994). «Синтаксический подход к правильности типов» . Информация и вычисления . 115 (1): 38–94. дои : 10.1006/inco.1994.1093 .
• Макракис, Ставрос (апрель 1982 г.). «Безопасность и мощность». Заметки по разработке программного обеспечения ACM SIGSOFT . 7 (2): 25–26. дои : 10.1145/1005937.1005941 . S2CID   10426644 .