bamalip: (NGE)
По поводу ветки (где я общаюсь с [livejournal.com profile] sassa_nf и [livejournal.com profile] pbl) помню, было когда-то обсуждение в рассылке по Идрису: какому тайпклассу должны соответствовать встроенные вещественные числа IEEE стандарта? Если делать по-честному, то это не будет настоящее алгебраическое поле. А что это? Есть (конечное) множество, операции на нем. Но нет алгебраической структуры, под которую эти операции подходят.

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

Может меня кто-то сейчас просветит? :)

Дополню цитатой из Воеводского: "Прикладная математика, может быть жестко так говорить, но она находится в состоянии жестокого застоя. По сути своей они используют модели, которым по 50 лет, слегка модифицируют, подгоняют под современные задачи."
bamalip: (NGE)
прошлогодняя дыра в xen, позволяющая писать эксплойты в том числе для некоторых средств, считающих себя суперзащищенными.

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


Admittedly this is subtle bug, because there is no buggy code that
could be spotted immediately. The bug emerges only if one looks at a
bigger picture of logic flows (compare also QSB #09 for a somehow
similar situation).

On the other hand, it is really shocking that such a bug has been
lurking in the core of the hypervisor for so many years. In our
opinion the Xen project should rethink their coding guidelines and try
to come up with practices and perhaps additional mechanisms that would
not let similar flaws to plague the hypervisor ever again (assert-like
mechanisms perhaps?). Otherwise the whole project makes no sense, at
least to those who would like to use Xen for security-sensitive work.

Specifically, it worries us that, in the last 7 years (i.e. all the
time when the bug was sitting there having a good time) so much
engineering and development effort has been put into adding all sorts
of new features and whatnots, yet no serious effort to improve Xen
security effectively. Because there have been, of course, many more
security bugs found in Xen over the last years (as the numbering of
this XSA suggests).

Profile

bamalip: (Default)
шерстяной ленин

July 2017

S M T W T F S
       1
2 3 4 56 7 8
9 1011 12 13 14 15
161718 19 2021 22
23242526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 22nd, 2017 06:44 pm
Powered by Dreamwidth Studios