Безопасность доступа к памяти

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

Языки программирования с низким уровнем абстракций, такие как Си и Си++, поддерживающие непосредственный доступ к памяти компьютера (произвольную арифметику указателей, выделение и освобождение памяти) и приведение типов, но не имеющие автоматической проверки границ[англ.] массивов, не являются безопасными с точки зрения доступа к памяти[1][2]. C и C++, тем не менее, содержат инструменты (такие как умные указатели), позволяющие повысить безопасность доступа к памяти. Этой же цели служат техники управления памятью[3]. Тем не менее, избежать ошибок доступа к памяти, особенно в сложных системах, зачастую не удаётся[4].

Уязвимости, связанные с доступом к памяти

править

Одним из наиболее распространённых классов уязвимостей программного обеспечения являются проблемы безопасности памяти[5][6]. Данный тип уязвимости известен с 1980-х годов[7]. Безопасность памяти подразумевает предотвращение попыток использовать или модифицировать данные, если это не было намерено разрешено программистом при создании программного продукта[8].

Множество критических с точки зрения производительности программ реализованы на языках программирования c низким уровнем абстракций (Си и Си++), которые склонны к появлению уязвимостей данного типа. Отсутствие защищённости этих языков программирования позволяет атакующим получить полный контроль над программой, изменять поток управления, иметь несанкционированный доступ к конфиденциальной информации[9]. На данный момент предложены различные решения проблем, связанных с доступом к памяти. Механизмы защиты должны быть эффективны одновременно как с точки зрения безопасности, так и с точки зрения производительности[10].

Первую огласку ошибки памяти получили в 1972 году[11]. И далее они являлись проблемой многих программных продуктов, средством, позволяющим применять эксплоиты. Например, червь Морриса использовал множество уязвимостей, часть из которых была связана с ошибками работы с памятью[12].

Типы ошибок памяти

править

Различают несколько видов ошибок памяти (уязвимостей), которые могут возникать в некоторых языках программирования[13][14][15]:

  • Нарушение границ массивов[англ.] — выражение, индексирующее массив, выходит из диапазона значений, установленного при определении этого массива. Отдельно выделяется особый подтип — ошибка неучтённой единицы[16]. Встречается при отсутствии проверок границ массивов и строк (Си, Си++)[17].
    • Переполнение буфера — запись за пределами выделенного в памяти буфера. Возникает при попытке записи в буфер блока данных, превышающего размер этого буфера. В результате переполнения могут быть испорчены данные, расположенные рядом с буфером[18], либо программа вовсе изменит своё поведение, вплоть до интерпретации записанных данных как исполняемого кода[19]. Использование данной уязвимости является одним из наиболее популярных способов взлома компьютерных систем[20].
    • Чтение за границами буфера[англ.] — чтение за пределами выделенного в памяти буфера. Последствиями могут служить нарушения безопасности системы (утрата конфиденциальности), нестабильное и неправильное поведение программы, ошибки прав доступа к памяти[21]. Эта уязвимость входит в список наиболее распространённых и опасных ошибок в программном обеспечении[22].
  • Ошибки при работе с динамической памятью — неправильное распоряжение динамически выделяемой памятью и указателями. В данном случае выделение памяти под объекты осуществляется во время выполнения программы[23], что может повлечь за собой ошибки времени исполнения. Данной уязвимости подвержены языки программирования с низким уровнем абстракций, поддерживающие непосредственный доступ к памяти компьютера (Си, Си++)[24].
    • Висячий указатель[25] — указатель, не ссылающийся на допустимый объект соответствующего типа. Данный вид указателей возникает, когда объект был удалён (или перемещён), но значение указателя не изменили на нулевое. В данном случае он всё ещё указывает на область памяти, где находился данный объект. В некоторых случаях это может стать причиной получения конфиденциальной информации злоумышленником; либо, если система уже перераспределила адресуемую память под другой объект, доступ по висячему указателю может повредить расположенные там данные[26]. Особый подтип ошибки — использование после освобождения (use after free) (обращение к освобождённой области памяти) — является распространённой причиной ошибок программ[27], например, уязвимостей веб-обозревателей[28].
    • Обращение по нулевому указателю. Нулевой указатель имеет специальное зарезервированное значение, показывающее, что данный указатель не ссылается на допустимый объект[29]. Обращение по нулевому указателю будет причиной исключительной ситуации[30] и аварийной остановки программы.
    • Освобождение ранее не выделенной памяти — попытка освободить область оперативной памяти, которая не является на данный момент выделенной (то есть свободна). Наиболее часто это проявляется в двойном освобождении памяти[31], когда происходит повторная попытка освободить уже освобождённую память. Данное действие может вызвать ошибку менеджера памяти[32]. В Си это происходит при повторном вызове функции free с одним и тем же указателем, без промежуточного выделения памяти.
    • Использование различных менеджеров памяти — ошибка, заключающаяся в разрыве связки аллокатор-деаллокатор памяти и использованием различных средств для работы с одним сегментом. Например, в Си++ использованием free для участка памяти, выделенного с помощью new или, аналогично, использованием delete после malloc. Стандарт Си++ не описывает какую-либо связь между new / delete и функциями работы с динамической памятью из Си, хотя new / delete в общем случае реализованы как обёртки malloc / free[33][34]. Смешанное использование может стать причиной неопределённого поведения[35].
    • Потеря указателя — утеря адреса выделенного фрагмента памяти при перезаписи его новым значением, который ссылается на другую область памяти[36]. При этом адресуемая предыдущим указателем память более недосягаема. Такой тип ошибки приводит к утечкам памяти, так как выделенная память не может быть освобождена. В Си это может случиться при повторном присваивании результата функции malloc одному и тому же указателю, без промежуточного освобождения памяти.
  • Неинициализированные переменные[англ.] — переменные, которые были объявлены, но не установлены в какое-либо значение, известное до времени их использования. Переменные будут иметь значение, но, в общем случае, труднопредсказуемое. Уязвимость для памяти могут возникнуть при наличии неинициализированных («диких») указателей[37]. Эти указатели в своём поведении схожи с висячими указателями, попытка обращения по ним в большинстве случаев будет сопровождаться ошибками доступа или повреждением данных. Однако, возможно получение конфиденциальной информации, которая могла остаться в данной области памяти после предыдущего использования[38][39].
  • Ошибки нехватки памяти — проблемы, возникающие при недостатке количества доступной памяти для данной программы.
    • Переполнение стека — превышение программой количества информации, которое может находиться в стеке вызовов (указатель вершины стека выходит за границу допустимой области). При этом программа аварийно завершается[40]. Причиной ошибки может быть глубокая (или бесконечная) рекурсия, либо выделение большого количества памяти для локальных переменных на стеке[41].
    • Переполнение кучи[англ.] — попытка программы выделить большее количество памяти, чем ей доступно. Является следствием частого (Java[42]) и зачастую неправильного обращения с динамической памятью. В случае возникновения ошибки, операционная система завершит наиболее подходящий с её точки зрения для этого процесс (часто, вызвавший ошибку, но иногда — произвольный[43]).

Обнаружение ошибок

править

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

Помимо предупреждений со стороны компилятора, для обнаружения ошибок до момента сборки программы используются статические анализаторы кода. Они позволяют покрыть значительную часть опасных ситуаций, исследуя исходный код более подробно, чем поверхностный анализ компилятора. Статические анализаторы могут обнаружить[44][45][46][47]:

  • Выход за границы массивов
  • Использование висячих (а также нулевых или неинициализированных) указателей
  • Неправильное использование библиотечных функций
  • Утечки памяти, как следствие неправильной работы с указателями

Во время отладки программы могут использоваться специальные менеджеры памяти. В данном случае вокруг аллоцированных в куче объектов создаются «мёртвые» области памяти, попадая в которые отладчик позволяет обнаружить ошибки[48]. Альтернативой являются специализированные виртуальные машины, проверяющие доступ к памяти (Valgrind). Обнаружить ошибки помогают системы инструментирования кода, в том числе обеспечиваемые компилятором (Sanitizer[49]).

Способы обеспечения безопасности

править

Большинство языков высокого уровня решают эти проблемы с помощью удаления из языка арифметики указателей, ограничением возможностей приведения типов, а также введением сборки мусора, как единственной схемы управления памятью[50]. В отличие от низкоуровневых языков, где важна скорость, высокоуровневые в большинстве своём осуществляют дополнительные проверки[51], например проверки границ при обращениях к массивам и объектам[52].

Чтобы избежать утечек памяти и ресурсов, обеспечить безопасность в плане исключений, в современном Си++ используются умные указатели. Обычно они представляют собой класс, имитирующий интерфейс обыкновенного указателя и добавляющего дополнительную функциональность[53], например проверку границ массивов и объектов, автоматическое управление выделением и освобождением памяти для используемого объекта. Они помогают реализовать идиому программирования Получение ресурса есть инициализация (RAII), заключающуюся в том, что получение объекта неразрывно связано с его инициализацией, а освобождение — с его уничтожением[54].

При использовании библиотечных функций следует уделять внимание возвращаемым ими значениям, чтобы обнаружить возможные нарушения в их работе[55]. Функции для работы с динамической памятью в Си сигнализируют об ошибке (нехватке свободной памяти запрашиваемого размера), возвращая вместо указателя на блок памяти нулевой указатель[56]; в Си++ используются исключения[57]. Правильная обработка данных ситуаций позволяет избежать неправильного (аварийного) завершения программы[58].

Повышению безопасности способствуют проверки границ при использовании указателей. Подобные проверки добавляются во время компиляции и могут замедлять работу программ; для их ускорения были разработаны специальные аппаратные расширения (например, Intel MPX[59]).

На нижних уровнях абстракций существуют специальные системы, обеспечивающие безопасность памяти. На уровне операционной системы это менеджер виртуальной памяти, разделяющий доступные области памяти для отдельных процессов (поддержка многозадачности), и средства синхронизации для поддержания многопоточности[60]. Аппаратный уровень также, как правило, включают некоторые механизмы, такие как кольца защиты[61].

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

Примечания

править
  1. Erik Poll. Lecture Notes on Language-Based Security. — Radboud University Nijmegen, 2016. — 21 Января. Архивировано 14 сентября 2016 года. / «Language features that break memory safety include …»
  2. Laszlo Szekeres, Mathias Payer, Dawn Song. SoK: Eternal War in Memory. — 2013 IEEE Symposium on Security and Privacy, 2013. Архивировано 5 августа 2021 года. / «Memory corruption bugs in software written in low-level languages like C or C++ are one of the oldest problems in computer security.»
  3. ISO Standard C++ Foundation. C++ FAQ: Memory Management (англ.). isocpp.org. Дата обращения: 10 февраля 2022. Архивировано 10 сентября 2018 года.
  4. ISO Standard C++ Foundation. C++ FAQ: Memory Management (англ.). isocpp.org. Дата обращения: 10 февраля 2022. Архивировано 10 сентября 2018 года. / «Clearly, if your code has new operations, delete operations, and pointer arithmetic all over the place, you are going to mess up somewhere and get leaks, stray pointers, etc. This is true independently of how conscientious you are with your allocations: eventually the complexity of the code will overcome the time and effort you can afford.»
  5. Victor van der Veen, Nitish dutt-Sharma, Lorenzo Cavallaro, Herbert Bos. Memory Errors: The Past, the Present, and the Future. — RAID’12; Amsterdam, The Netherlands, 2012. — 12—14 Сентября. Архивировано 26 июня 2016 года. / «… and still rank among the top 3 most dangerous software errors.»
  6. Dawn Song. Memory safety — Attacks and Defenses. — Berkeley CS161 Computer Security, 2015. — Весна. Архивировано 1 марта 2015 года. / «In fact, after configuration errors, implementation errors are probably the largest single class of security errors exploited in practice.»
  7. Laszlo Szekeres, Mathias Payer, Dawn Song. SoK: Eternal War in Memory. — 2013 IEEE Symposium on Security and Privacy, 2013. Архивировано 5 августа 2021 года. / «This problem has existed for more than 30 years …»
  8. Dawn Song. Memory safety — Attacks and Defenses. — Berkeley CS161 Computer Security, 2015. — Весна. Архивировано 1 марта 2015 года. / «… preventing attackers from reading or writing to memory locations other than those intended by the programmer.»
  9. Laszlo Szekeres, Mathias Payer, Dawn Song. SoK: Eternal War in Memory. — 2013 IEEE Symposium on Security and Privacy, 2013. Архивировано 5 августа 2021 года. / «Applications written in low-level languages like C or C++ are prone to these kinds of bugs. The lack of memory safety … enables attackers to exploit memory bugs by maliciously altering the program’s behavior or even taking full control over the control-flow.»
  10. Laszlo Szekeres, Mathias Payer, Dawn Song. SoK: Eternal War in Memory. — 2013 IEEE Symposium on Security and Privacy, 2013. Архивировано 5 августа 2021 года. / «… in finding the balance betweeneffectiveness(security)andefficiency.»
  11. Victor van der Veen, Nitish dutt-Sharma, Lorenzo Cavallaro, Herbert Bos. Memory Errors: The Past, the Present, and the Future. — RAID’12; Amsterdam, The Netherlands, 2012. — 12—14 Сентября. Архивировано 26 июня 2016 года. / «Memory errors were first publicly discussed in 1972 by the Computer Security Technology Planning Study Panel.»
  12. Victor van der Veen, Nitish dutt-Sharma, Lorenzo Cavallaro, Herbert Bos. Memory Errors: The Past, the Present, and the Future. — RAID’12; Amsterdam, The Netherlands, 2012. — 12—14 Сентября. Архивировано 26 июня 2016 года. / «The Internet Worm exploited a number of vulnerabilities, including memory error-related ones.»
  13. Laszlo Szekeres, Mathias Payer, Dawn Song. SoK: Eternal War in Memory. — 2013 IEEE Symposium on Security and Privacy, 2013. Архивировано 5 августа 2021 года.
  14. Dawn Song. Memory safety — Attacks and Defenses. — Berkeley CS161 Computer Security, 2015. — Весна. Архивировано 1 марта 2015 года.
  15. Katrina Tsipenyuk, Brian Chess, Gary McGraw. Seven Pernicious Kingdoms: A Taxonomy of Software Security Errors. — NIST Workshop on Software Security Assurance Tools, Techniques, and Metrics, Long Beach, CA, 2005. — Ноябрь. Архивировано 7 октября 2016 года.
  16. Edsger W. Dijkstra. Why numbering should start at zero (EWD 831). — Plataanstraat 5, 5671 AL NUENEN, The Netherlands, 1982. — 11 Августа. Архивировано 16 сентября 2016 года. / «… the use of the other three conventions has been a constant source of clumsiness and mistakes …»
  17. Richard Jones and Paul Kelly. Bounds Checking for C. — Imperial College, 1995. — Июль. Архивировано 26 марта 2016 года. / «One response to this analysis is to discard C, since this lack of efficient checkability is responsible for many software failures.»
  18. Джон Эриксон. Хакинг. Искусство эксплойта. — СПб.: Символ-Плюс, 2010. — С. 139. — ISBN 978-5-93286-158-5.
  19. Джон Эриксон. Хакинг. Искусство эксплойта. — СПб.: Символ-Плюс, 2010. — С. 142. — ISBN 978-5-93286-158-5.
  20. David A. Wheeler. Secure Programming HOWTO. — Published v3.72. — 2015. Архивировано 28 мая 2016 года. / «Buffer overflows are an extremely common and dangerous security flaw …»
  21. Common Weakness Enumeration. CWE-126: Buffer Over-read (8 декабря 2015). Дата обращения: 24 ноября 2016. Архивировано 27 сентября 2016 года. / «This typically occurs when the pointer or its index is incremented to a position beyond the bounds of the buffer …»
  22. Steve Christey. 2011 CWE/SANS Top 25 Most Dangerous Software Errors. MITRE (13 сентября 2011). Дата обращения: 24 ноября 2016. Архивировано 12 апреля 2018 года.
  23. Guy Keren. Unix And C/C++ Runtime Memory Management For Programmers (2001—2002). Дата обращения: 24 ноября 2016. Архивировано из оригинала 27 сентября 2016 года. / «The runtime environment defines not only how memory is allocated and freed …»
  24. Robert C. Seacord. Secure Coding in C and C++. — Addison-Wesley, 2013. — P. 162. — ISBN 978-0-321-82213-0.
  25. Jonathan Afek, Adi Sharabani. Dangling Pointer. Smashing the Pointer for Fun and Profit. — Watchfire Corporation, 2007. Архивировано 19 февраля 2018 года.
  26. Компьютерная газета. Ссылка в никуда, или сломанный указатель. Дата обращения: 24 ноября 2016. Архивировано 22 июня 2018 года. / «… уязвимости, к которым может привести неправильное использование указателей и ссылок.»
  27. Common Weakness Enumeration. CWE-416: Use After Free (8 декабря 2015). Дата обращения: 24 ноября 2016. Архивировано 18 июля 2019 года. / «Referencing memory after it has been freed can cause a program to crash, use unexpected values, or execute code.»
  28. Juan Caballero, Gustavo Grieco, Mark Marron, Antonio Nappa. Undangle: Early Detection of Dangling Pointers in Use-After-Free and Double-Free Vulnerabilities. — IMDEA Software Institute; Madrid, Spain. Архивировано 10 сентября 2016 года. / «Use-after-free vulnerabilities are rapidly growing in popularity, especially for exploiting web browsers.»
  29. comp.lang.c. Question 5.1. Дата обращения: 24 ноября 2016. Архивировано 27 сентября 2016 года. / «The language definition states that for each pointer type, there is a special value …»
  30. Oracle. Java Platform, Standard Edition 7 API Specification. Дата обращения: 24 ноября 2016. Архивировано 23 апреля 2018 года. / «Thrown when an application attempts to use null in a case where an object is required.»
  31. Common Weakness Enumeration. CWE-415: Double Free (8 декабря 2015). Дата обращения: 24 ноября 2016. Архивировано 27 сентября 2016 года. / «When a program calls free() twice with the same argument …»
  32. Yan Huang. Heap Overflows and Double-Free Attacks. Дата обращения: 24 ноября 2016. Архивировано 17 апреля 2018 года. / «If free(p) has already been called before, undefined behavior occurs.»
  33. Andrei Alexandrescu. Modern C++ Design: Generic Programming and Design Patterns Applied. — Addison Wesley, 2001. (недоступная ссылка) / «… it is usually implemented as a thin wrapper around the C heap allocator …»
  34. Guy Keren. Unix And C/C++ Runtime Memory Management For Programmers (2001—2002). Дата обращения: 25 ноября 2016. Архивировано из оригинала 27 сентября 2016 года. / «For example, the GNU C++ compiler’s new operator actually invokes the C runtime malloc() function.»
  35. Memory Management. Дата обращения: 25 ноября 2016. Архивировано 10 сентября 2018 года. / «The C++ operators new and delete guarantee proper construction and destruction … The C-style functions … don’t ensure that.»
  36. OWASP. Memory leak. Дата обращения: 25 ноября 2016. Архивировано 23 ноября 2016 года.
  37. Проблемы, связанные с указателями. Дата обращения: 25 ноября 2016. Архивировано 26 февраля 2013 года. / «Ничто так не беспокоит, как „дикие“ указатели!»
  38. Halvar Flake. Attacks on uninitialized local variables (2006). Дата обращения: 25 ноября 2016. Архивировано 3 июня 2016 года. / «We’re looking at the following situation then …»
  39. Common Weakness Enumeration. CWE-457: Use of Uninitialized Variable (8 декабря 2015). Дата обращения: 25 ноября 2016. Архивировано 2 октября 2016 года. / «An attacker can sometimes control or read these contents.»
  40. Using and Porting GNU Fortran. James Craig, Burley (1 июня 1991). Дата обращения: 25 ноября 2016. Архивировано 5 октября 2012 года.
  41. Danny Kalev. Understanding Stack Overflow (5 сентября 2000). Дата обращения: 25 ноября 2016. Архивировано 5 октября 2012 года. / «The two most common causes for a stack overflow …»
  42. John Boyland. Position Paper: Handling „Out Of Memory“ Errors. — University of Wisconsin-Milwaukee, USA. Архивировано 22 марта 2016 года. / «An „out of memory“ error can be catastrophic for a program, especially one written in a language such as Java that uses memory allocation frequently.»
  43. Mulyadi Santosa. When Linux Runs Out of Memory (30 ноября 2006). Дата обращения: 15 ноября 2016. Архивировано 14 апреля 2018 года. / «… you can no longer allocate more memory and the kernel kills a task (usually the current running one).»
  44. Anders Moller and Michael I. Schwartzbach. Static Program Analysis. — Department of Computer Science, Aarhus University, 2015. — Май. Архивировано 11 февраля 2017 года.
  45. Cppcheck — A tool for static C/C++ code analysis. Дата обращения: 25 ноября 2016. Архивировано 18 января 2016 года. / «Detect various kinds of bugs in your code …»
  46. Semantic Designs. Memory Safety analysis with CheckPointer. Дата обращения: 25 ноября 2016. Архивировано 18 апреля 2018 года. / «Programs with pointers can commit a variety of errors in accessing memory …»
  47. PVS-Studio. Статический анализ кода (25 марта 2015). Дата обращения: 25 ноября 2016. Архивировано 25 января 2018 года.
  48. Emery D. Berger, Benjamin G. Zorn. DieHard: Probabilistic Memory Safety for Unsafe Languages. — PLDI’06; Ottawa, Ontario, Canada, 2006. — 11-14 Июня. Архивировано 6 марта 2016 года.
  49. Konstantin Serebryany, Dmitry Vyukov. Finding races and memory errors with compiler instrumentation. GNU Tools Cauldron (10 июля 2012). Дата обращения: 25 ноября 2016. Архивировано 12 марта 2016 года.
  50. Erik Poll. Language-based Security: 'Safe' programming languages. Radboud Universiteit Nijmegen. Дата обращения: 25 ноября 2016. Архивировано из оригинала 5 ноября 2016 года. / «Manual memory management can be avoided by …»
  51. Dinakar Dhurjati and Vikram Adve. Backwards-Compatible Array Bounds Checking for C with Very Low Overhead. — Department of Computer Science University of Illinois at Urbana-Champaign. Архивировано 1 июля 2016 года. / «… an unsolved problem despite a long history of work on detecting array bounds violations or buffer overruns, because the best existing solutions to date are either far too expensive for use in deployed production code …»
  52. Bruce Eckel. Thinking in Java. Fourth Edition. Архивировано 19 ноября 2016 года. / «Both arrays and containers guarantee that you can’t abuse them. Whether you’re using an array or a container, you’ll get a RuntimeException if you exceed the bounds, indicating a programmer error.»
  53. David Kieras. Using C++11’s Smart Pointers. — EECS Department, University of Michigan, 2016. — Июнь. Архивировано 30 ноября 2016 года. / «Smart pointers are class objects that behave like built-in pointers but also manage objects that you create …»
  54. Microsoft Developer Network. Интеллектуальные указатели (современный C++). Дата обращения: 25 ноября 2016. Архивировано 5 декабря 2017 года. / «Они чрезвычайно важны для идиомы программирования RAII или Resource Acquisition Is Initialialization …»
  55. Common Weakness Enumeration. CWE-252: Unchecked Return Value (8 декабря 2015). Дата обращения: 25 ноября 2016. Архивировано 18 июля 2019 года. / «The software does not check the return value from a method or function, which can prevent it from detecting unexpected states and conditions.»
  56. Microsoft Developer Network. malloc. Дата обращения: 25 ноября 2016. Архивировано 5 октября 2016 года. / «malloc возвращает нетипизированный указатель на выделенную область памяти или NULL, если недоступно достаточно памяти.»
  57. operator new, operator new[]. Дата обращения: 25 ноября 2016. Архивировано 29 марта 2018 года. / «throws std::bad_alloc or another exception derived from std::bad_alloc (since C++11) on failure to allocate memory»
  58. Paul and Harvey Deitel. C : how to program. Архивировано 2 октября 2015 года.
  59. Intel Developer Zone. Introduction to Intel® Memory Protection Extensions (16 июля 2013). Дата обращения: 25 ноября 2016. Архивировано 5 мая 2019 года.
  60. Sarah Diesburg. Memory Protection: Kernel and User Address Spaces. Дата обращения: 25 ноября 2016. Архивировано 9 августа 2017 года.
  61. Michael D. Schroeder and Jerome H. Saltzer. A Hardware Architecture for Implementing Protection Rings. — Third ACM Symposium on Operating Systems Principles, Palo Alto, California, 1971. — 18-20 Октября. Архивировано 25 февраля 2021 года.
  62. Kolanski, Rafal Michal. Verification of Programs in Virtual Memory Using Separation Logic. — PhD. — Australia : University of New South Wales (UNSW), 2011.

Литература

править

Ссылки

править

Общие публикации

Тематические публикации