Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation
The present and the previous article on Realistic Correct Systems Implementation together address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we want to ask: Can informaticians righteously be accounted for incorr...
Збережено в:
| Дата: | 2003 |
|---|---|
| Автори: | , |
| Формат: | Стаття |
| Мова: | Англійська |
| Опубліковано: |
Інститут програмних систем НАН України
2003
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/1304 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation / Wolfgang Goerigk, Hans Langmaack // Проблеми програмування. — 2003. — N 2. — С. 3—27. — Бібліогр.: 37 назв. — англ. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859531909130878976 |
|---|---|
| author | Goerigk, Wolfgang Langmaack, Hans |
| author_facet | Goerigk, Wolfgang Langmaack, Hans |
| citation_txt | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation / Wolfgang Goerigk, Hans Langmaack // Проблеми програмування. — 2003. — N 2. — С. 3—27. — Бібліогр.: 37 назв. — англ. |
| collection | DSpace DC |
| description | The present and the previous article on Realistic Correct Systems Implementation together address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we want to ask: Can informaticians righteously be accounted for incorrectness of ystems, will they be able to justify systems to work correctly as intended? We understand the word justification in this sense, i.e. for the design of computer based systems, the formulation of mathematical models of information flows, and the construction of controlling software to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external attacks are foreseeable as logical consequences of the models. Since more than 40 years, theoretical informatics, software engineering and compiler construction have made important contributions to correct specification and also to correct high-level implementation of compilers. But the third step, translation — bootstrapping — of high level compiler programs into host machine code by existing host ompilers, is as important. So far there are no realistic recipes to close this gap, although it is known for many years that trust in executable code can dangerously be compromised by Trojan Horses in compiler executables, even if they pass strongest tests. Our article will show how to close this low level gap. We demonstrate the method of rigorous syntactic a-posteriori code inspection, which has been developed by the research group Verifix funded by the Deutsche Forschungsgemeinschaft (DFG).
Багато років теоретична інформатика вчастині розробки програмного забезпечення і побудови компіляторів займалась проблемами правильності специфікацій і високорівневих реалізацій компіляторів. У другій частині статті розглядається проблема коректного і безпечного перекладу (bootstrapping) програм з мови високого рівня в коди машини. Показано, як вирішуються проблеми коректності програм на мовах низького рівня. Продемонстрований метод строго синтаксичного апостеріор ного аналізу, котрий був розроблений дослідною групою Verifix в університеті м. Киля (ФРН).
Много лет теоретическая информатика в части разработки программного обеспечения и построения компиляторов занималась проблемами правильности спецификаций и высокоуровневых реализаций компиляторов. Во второй части статьи рассматривается проблема корректного и безопасного перевода (bootstrapping) программ с языка высокого уровня в коды машины. Показано, как решаются проблемы корректности программ на языках низкого уровня. Продемонстрирован метод строго синтаксического апостериорного анализа, который был разработан исследовательской группой Verifix в университете г. Киля (ФРГ).
|
| first_indexed | 2025-11-25T22:46:37Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-1304 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | English |
| last_indexed | 2025-11-25T22:46:37Z |
| publishDate | 2003 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Goerigk, Wolfgang Langmaack, Hans 2008-07-24T16:54:52Z 2008-07-24T16:54:52Z 2003 Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation / Wolfgang Goerigk, Hans Langmaack // Проблеми програмування. — 2003. — N 2. — С. 3—27. — Бібліогр.: 37 назв. — англ. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/1304 681.3.51 The present and the previous article on Realistic Correct Systems Implementation together address correct construction and functioning of large computer based systems. In view of so many annoying and dangerous system misbehaviors we want to ask: Can informaticians righteously be accounted for incorrectness of ystems, will they be able to justify systems to work correctly as intended? We understand the word justification in this sense, i.e. for the design of computer based systems, the formulation of mathematical models of information flows, and the construction of controlling software to be such that the expected system effects, the absence of internal failures, and the robustness towards misuses and malicious external attacks are foreseeable as logical consequences of the models. Since more than 40 years, theoretical informatics, software engineering and compiler construction have made important contributions to correct specification and also to correct high-level implementation of compilers. But the third step, translation — bootstrapping — of high level compiler programs into host machine code by existing host ompilers, is as important. So far there are no realistic recipes to close this gap, although it is known for many years that trust in executable code can dangerously be compromised by Trojan Horses in compiler executables, even if they pass strongest tests. Our article will show how to close this low level gap. We demonstrate the method of rigorous syntactic a-posteriori code inspection, which has been developed by the research group Verifix funded by the Deutsche Forschungsgemeinschaft (DFG). Багато років теоретична інформатика вчастині розробки програмного забезпечення і побудови компіляторів займалась проблемами правильності специфікацій і високорівневих реалізацій компіляторів. У другій частині статті розглядається проблема коректного і безпечного перекладу (bootstrapping) програм з мови високого рівня в коди машини. Показано, як вирішуються проблеми коректності програм на мовах низького рівня. Продемонстрований метод строго синтаксичного апостеріор ного аналізу, котрий був розроблений дослідною групою Verifix в університеті м. Киля (ФРН). Много лет теоретическая информатика в части разработки программного обеспечения и построения компиляторов занималась проблемами правильности спецификаций и высокоуровневых реализаций компиляторов. Во второй части статьи рассматривается проблема корректного и безопасного перевода (bootstrapping) программ с языка высокого уровня в коды машины. Показано, как решаются проблемы корректности программ на языках низкого уровня. Продемонстрирован метод строго синтаксического апостериорного анализа, который был разработан исследовательской группой Verifix в университете г. Киля (ФРГ). en Інститут програмних систем НАН України Теоретические и методологические основы программирования Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation Чи здатна інформатика обґрунтовувати побудову великих комп’ютерних систем? Частина II. Доказова побудова компіляторів Cпособна ли информатика обосновывать построение больших компьютерных систем? Часть II. Доказательное построение компиляторов Article published earlier |
| spellingShingle | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation Goerigk, Wolfgang Langmaack, Hans Теоретические и методологические основы программирования |
| title | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_alt | Чи здатна інформатика обґрунтовувати побудову великих комп’ютерних систем? Частина II. Доказова побудова компіляторів Cпособна ли информатика обосновывать построение больших компьютерных систем? Часть II. Доказательное построение компиляторов |
| title_full | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_fullStr | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_full_unstemmed | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_short | Will Informatics be able to Justify the Construction of Large Computer Based Systems? Part II. Trusted compiler implementation |
| title_sort | will informatics be able to justify the construction of large computer based systems? part ii. trusted compiler implementation |
| topic | Теоретические и методологические основы программирования |
| topic_facet | Теоретические и методологические основы программирования |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/1304 |
| work_keys_str_mv | AT goerigkwolfgang willinformaticsbeabletojustifytheconstructionoflargecomputerbasedsystemspartiitrustedcompilerimplementation AT langmaackhans willinformaticsbeabletojustifytheconstructionoflargecomputerbasedsystemspartiitrustedcompilerimplementation AT goerigkwolfgang čizdatnaínformatikaobgruntovuvatipobudovuvelikihkompûternihsistemčastinaiidokazovapobudovakompílâtorív AT langmaackhans čizdatnaínformatikaobgruntovuvatipobudovuvelikihkompûternihsistemčastinaiidokazovapobudovakompílâtorív AT goerigkwolfgang cposobnaliinformatikaobosnovyvatʹpostroeniebolʹšihkompʹûternyhsistemčastʹiidokazatelʹnoepostroeniekompilâtorov AT langmaackhans cposobnaliinformatikaobosnovyvatʹpostroeniebolʹšihkompʹûternyhsistemčastʹiidokazatelʹnoepostroeniekompilâtorov |