Хабрахабр

[Перевод] Курс MIT «Безопасность компьютерных систем». Лекция 11: «Язык программирования Ur/Web», часть 3

Массачусетский Технологический институт. Курс лекций #6.858. «Безопасность компьютерных систем». Николай Зельдович, Джеймс Микенс. 2014 год

Computer Systems Security — это курс о разработке и внедрении защищенных компьютерных систем. Лекции охватывают модели угроз, атаки, которые ставят под угрозу безопасность, и методы обеспечения безопасности на основе последних научных работ. Темы включают в себя безопасность операционной системы (ОС), возможности, управление потоками информации, языковую безопасность, сетевые протоколы, аппаратную защиту и безопасность в веб-приложениях.

Лекция 1: «Вступление: модели угроз» Часть 1 / Часть 2 / Часть 3
Лекция 2: «Контроль хакерских атак» Часть 1 / Часть 2 / Часть 3
Лекция 3: «Переполнение буфера: эксплойты и защита» Часть 1 / Часть 2 / Часть 3
Лекция 4: «Разделение привилегий» Часть 1 / Часть 2 / Часть 3
Лекция 5: «Откуда берутся ошибки систем безопасности» Часть 1 / Часть 2
Лекция 6: «Возможности» Часть 1 / Часть 2 / Часть 3
Лекция 7: «Песочница Native Client» Часть 1 / Часть 2 / Часть 3
Лекция 8: «Модель сетевой безопасности» Часть 1 / Часть 2 / Часть 3
Лекция 9: «Безопасность Web-приложений» Часть 1 / Часть 2 / Часть 3
Лекция 10: «Символьное выполнение» Часть 1 / Часть 2 / Часть 3
Лекция 11: «Язык программирования Ur/Web» Часть 1 / Часть 2 / Часть 3

Такой вариант не разрешён, потому что подобное не допускается. Последнее, что нам нужно сделать и что будет весьма поучительно – это изменить этот код, указав там модуль комнаты, а затем попытаться получить доступ к таблице комнаты, как в предыдущем примере.

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

Мы могли бы упомянуть этот дополнительный модуль, который мы создали просто для удовольствия.

Мы можем без проблем получить к нему доступ. Но тогда это будут разные таблицы. Поэтому я разобью это на две части, мы начнем с того, что просто вызовем метод room, а затем сделаем немного другую вещь, чтобы прочитать его элементы.

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

То есть сейчас у нас есть эта инкапсуляция, поэтому вы можете думать о структуре этой комнаты, как о библиотеке, но вам не нужно об этом беспокоиться.

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

Студент: итак, вы изменили определение комнаты, что в этом случае произойдёт с таблицей базы данных?

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

Студент: но это не будет автоматически удалять базу данных или что-то в этом роде?

Я не думаю, что компилятор должен это делать. Профессор: надеюсь, что нет. Я думаю, что вам нужно написать команды alter table для запуска, потому что компилятор сейчас этого не делает. Вы можете представить себе настройку компилятора для понимания эволюции базы данных.

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

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

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

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

И я также наложу на неё ограничение, говорящее о том, что ключом к ней является форма ID. Я собираюсь разместить таблицу прямо в подписи.

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

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

Давайте сделаем то же самое для пароля. Мы не собираемся применять другое разрешение, потому что не хотим иметь возможность превращать ID обратно во что-то другое. Мы хотим иметь возможность прочитать пароль пользователя, но не собираемся принимать пароль и превращать его в строку, которая скажет нам, что пользователь вошёл в чат.

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

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

А дальше следует сюрприз. Первый шаг – мы просто копируем это определение. Оказывается, что ID и пароли пользователей – это строки, но вне модуля это обстоятельство раскрыто не будет.

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

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

Другие части кода не смогут прочитать cookie, потому что у них просто нет этого приватного поля. Эти кукиз являются приватными для данного модуля. Но они будут сохранятся при просмотре различных страниц, как это бывает с обычными кукиз. Так что никто не сможет напрямую увидеть ID и пароль, которые сохранены для этого пользователя.

Этот процесс как раз проверит, сможем ли мы найти строку в базе данных, в которой имеются этот идентификатор пользователя ID и пароль. Сейчас я вставлю функцию login, которая запустит процесс, чтобы проверить базу данных и узнать, действительно ли это правильная пара имени пользователя и пароля.

Давай просто сохраним это в кукиз. Если мы найдем её, то хорошо, значит, это правильное значение. И мы должны расположить некоторые вещи здесь, для простоты я скажу, что этот cookie не имеет срока действия. Мы используем метод, изменяющий значение cookie. Я не хочу запускать здесь SSL, поэтому скажу, что в данном случае безопасность нам не нужна, и задам параметр Secure = false.

Если проверка не удалась и модуль просигнализирует об ошибке, выполнение программы остановится, выдав описание этой ошибки. Но если вы действительно заботитесь о безопасности, очевидно, вы напишете Secure = true.

Это параметр также может иметь значение none, если пользователь еще не вошел в систему, и в этом случае мы получим другое сообщение об ошибке. Наконец, мы можем создать эту функцию, которая сообщает, какой конкретный пользователь вошел в систему, получив текущее значение cookie. Так что я просто скопирую её сюда и запущу ту же проверку. Или это может быть какая-то запись именно того типа, который мы использовали выше. Если это сработает, то мы просто вернём ту часть записи ID, которую мы только что проверили в базе данных.

Запускаем компилятор, и результат вы видите на экране. Итак, позвольте мне просто это проверить.

Но вне этого модуля мы думаем про это с точки зрения интерфейса. Главными здесь являются все эти детали реализации. Эта таблица пользователей выражает термины, разрешающие превратить строки в идентификаторы и пароли, но не наоборот. Есть некоторые неизвестные типы идентификаторов ID и паролей. Есть вопросы по этому поводу? У нас есть эти два метода ввода логина в первую очередь и есть проверка, какой именно пользователь вошел в систему на этом этапе.

Студент: нужно ли вам раскрывать таблицу пользователей?

Итак, мы почти на том этапе, когда я могу показать вам CSRF защиту в действии. Профессор: я делаю так, потому что я хочу использовать её позже в качестве внешнего ключа, так что это не важная причина.

Хорошо, что мы можем ещё сделать в этом месте программы? Начнём с того, что залогинимся в системе, это достаточно легко сделать. Здесь вы должны ввести имя пользователя и пароль и затем нажать на кнопку submit action. Давайте просто добавим сюда еще одну часть страницы, которая говорит, что это то место, где вы вводите логин. Это действие обеспечит вызов функции login.

На самом деле это просто оболочка вокруг вызова функции login из этого модуля, в котором мы берем каждый из компонентов и преобразуем его из строки в абстрактный тип. Давайте определим login как функцию, которая делает эти вещи.

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

У нас есть набор файлов cookie для записи этой информации, так что зайдём в комнату чата и отправим сообщение, например, asfasf. Теперь я могу войти в систему как пользователь а, поверьте мне на слово. Вы видите, что после нажатия на кнопку Add оно появилось в чате.

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

Когда мы отправляем эту форму, cookie не читается. Здесь есть кукиз, но система определила, что мы не используем кукиз. Итак, теперь мы должны добавить способ использования cookie и увидеть, как себя проявит защита. Таким образом, пока что нет никакой необходимости добавлять сюда защиту CSRF.

Студент: а что собой представляет содержание cookie?

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

Теперь давайте на самом деле используем куки. Так что это именно то, что содержится там в определенной сериализованной форме. Но мы будем вызывать методы пользовательского модуля, которые косвенно связаны с использованием файлов cookie. Мы должны это увидеть, несмотря на то, что будем использовать cookie косвенно, потому что мы собираемся использовать его в модуле room, который никакого отношения к куки не имеет. И тогда система поймет, что это означает то, что мы от неё зависим.

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

Я добавлю в пользовательский модуль идентификатор ID, и тогда это должно сработать, так как тип ID поддерживает проверку на равенство.

Теперь у нас всё должно быть в порядке, и мы можем проделать больше вещей с этим ID, который способен вызвать некоторые проблемы безопасности.

Это позволяет нам добавить проверку контроля доступа, так что давайте посмотрим, как это работает и вернёмся на главную страницу.

Теперь эти четыре буквы «а» появились и в чате.

Это sig подписывало кукиз, используя ключ, который является секретным для сервера. В консоли интерфейса мы видим, что теперь форма автоматически получила скрытое входное имя sig, которое является криптографической подписью значений всех файлов cookie. Для этого у нас есть операция say. А когда форма готова, приложение знает — потому что об этом ему сказал компилятор — что приложение должно проверять подписи для следующего набора операций.

Студент: имеют ли подписи что-то вроде штампа времени?

Профессор: нет, подписи не имеют временных меток.

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

Это то, что можно изменить, просто изменив реализацию языка без изменения приложений, а затем быстро развернуть. Профессор: да, он никогда не истекает. И я понимаю, почему это было бы полезно добавить. Но сейчас здесь этого нет.

Студент: вы также можете исправить это, просто поставив метку времени на подписи.

Профессор: да, вы правы, вы можете изменить приложение таким образом, чтобы намеренно изменять данные cookie достаточно часто, то есть сделать так, чтобы подпись устаревала.
Студент: вы можете переназначить URL-адреса?

Профессор: да, какие переназначения вы хотели бы увидеть?

Студент: любые, я просто хочу посмотреть, как это делается.

Предположим, что нам не нравится эта форма. Профессор: Итак, компилятор назначает… как мы видим, мы вызвали функцию say, и этот вызов функции сериализуется как определенная форма URL.

Лучше вставить это наверх. Мы решили, что мы собираемся переписать URL, так сказать, внутри модуля комнаты, внутри демо. Итак, мы хотим переназначить url Demo/Room/say в Demo/Room /Speak.

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

Существуют ли другие библиотеки для других форматов? Студент: вы упомянули, что HTML не является спецификой компилятора, это просто библиотека.

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

Студент: предположим, мы всё ещё хотим писать на JavaScript, например, чтобы анимировать какие-то вещи на странице …

В этой версии есть код на стороне клиента. Профессор: позвольте мне загрузить Ajax-версию этого, что позволит ответить на ваш вопрос. Я ввёл данные на главной странице в строку чата, и они так же появились внизу чата. Давайте просто перейдём на вариант программы под названием demo3. Это получается благодаря тегу кнопки button value. Хотите верьте, хотите нет, но на этот раз надстройка работала с помощью Ajax-вызова. У него есть атрибут onclick, который, когда пользователь нажимает кнопку, весь этот код ниже строки с данным атрибутом срабатывает на стороне клиента.

]

Компилятор переводит это для вас в JavaScript и гарантирует, что он сохраняет свойства, которые мы хотим иметь для абстракций в нашем списке, если пользователь не хочет возится с ним вручную в браузере. Но это код Ur/Web, это не код JavaScript.

Есть ли в них способ взаимодействия с JavaScript из Ur/Web? Студент: я думаю, что сегодня есть много библиотек, которые делают полезные вещи, и во многих случаях сложные вещи, если вы хотите всё перекодировать сами.

Но когда вы используете интерфейс внешней функции, вы больше не можете пользоваться всеми этими полезными функциями конструирования. Профессор: да, есть интерфейс внешних функций, который позволяет давать имена функций Ur/Web именам функций JavaScript и вызовам. В этом случае вы должны быть очень осторожными.

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

Но теперь, вместо того, чтобы вызывать её по ссылке, мы просто берем вызов функции, который заполняется аргументами, которые приходят из контекста обработчика onclick. У нас все еще есть та же функция say, что и раньше.

Это значит, что это функция вызова на стороне клиента, но сам вызов запускается на сервере с доступом к базе данных и другим ресурсам сервера, а затем переносит результат обратно сюда. Мы просто обернем эту функцию внутри синтаксиса rpc.

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

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

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

Вы действительно можете обеспечить подомное, потому что у нас здесь нет DOM. Давайте я приведу пример вызова метода этой абстракции из части страницы, которая отображает список строк текста, которые можно только добавить, но не удалить. Это совсем не то, когда любая часть кода может проникнуть в дерево документа и видоизменить его, изменить журнал и уничтожить ранее добавленные строки.

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

Итак, если больше нет вопросов, на этом мы завершим лекцию.

Студент: каналы?

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

Как вы смягчаете проблемы, которые создают сами слои абстракции? Студент: очень трудно писать правильные библиотеки и компиляторы.

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

Студент: почему вы выбрали такое имя для своего языка — Ur?

И идея в том, что этот язык позволяет вставлять внутрь него всякие другие языки. Профессор: Ur — это понятие из лингвистики, так назывался язык, который является предком современного языка. Так что это своего рода прародитель всех языков.

Полная версия курса доступна здесь.

Вам нравятся наши статьи? Спасибо, что остаётесь с нами. Поддержите нас оформив заказ или порекомендовав знакомым, 30% скидка для пользователей Хабра на уникальный аналог entry-level серверов, который был придуман нами для Вас: Вся правда о VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps от $20 или как правильно делить сервер? Хотите видеть больше интересных материалов? (доступны варианты с RAID1 и RAID10, до 24 ядер и до 40GB DDR4).

VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps до декабря бесплатно при оплате на срок от полугода, заказать можно тут.

класса c применением серверов Dell R730xd Е5-2650 v4 стоимостью 9000 евро за копейки? Dell R730xd в 2 раза дешевле? Только у нас 2 х Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 ТВ от $249 в Нидерландах и США! Читайте о том Как построить инфраструктуру корп.

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть