Description of Paralocks language semantics in TLA+

Texto integral

1. ВВЕДЕНИЕ

Статья будет полезна читателям, хорошо знакомым с формальными моделями безопасности компьютерных систем, основанными на управлении доступом и контроле информационных потоков (КИП), обладающим достаточными знаниями в области формальной верификации и навыками работы с соответствующими инструментальными средствами. Необходимую предварительную информацию можно получить, обратившись к источникам: [1]—[5].

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

В работе представлена семантика упрощенной версии языка описания политик безопасности Paralocks [4], лежащего в основе механизма КИП платформы PLIF [6], а также приводятся исчерпывающие пояснения к доказательствам свойств решетки, заданной на множестве всех возможных политик.

Для проверки обозначенных свойств применялся следующий подход. На предварительном этапе осуществлялся прогон модели на небольшом наборе исходных данных с использованием инструмента TLC. Отсутствие выявленных на этом этапе противоречий сделало оправданным переход ко второму этапу – доказательству свойств с использованием формальной логической системы TLAPS. Указанная система позволяет выстраивать доказательства в иерархическим стиле, который упрощает применение метода естественной дедукции. TLAPS опирается на инструменты автоматизированного доказательства теорем, такие как Isabelle [7], Zennon [8]. Описанный подход предоставляет дополнительные гарантии, что достаточно важно в области формальных моделей. По мнению некоторых авторов [9] до трети доказательств, предлагаемых в различных исследованиях, являются некорректными.

Отметим также, что определенной инновацией явилось использование подсистемы проверки типов Apalache [10] для доказательства инвариантов типов некоторых структур, используемых для описания предложений политик безопасности и самих политик в спецификациях TLA+. Это, в свою очередь, позволило обоснованно использовать в доказательствах некоторые неочевидные предположения.

2. СЕМАНТИКА PARALOCKS В TLA+

Язык описания политик безопасности в программной среде Paralocks [4] является основой перспективной платформы контроля информационных потоков в программных блоках баз данных PLIF. Преимущества языка, предопределившие его выбор, описаны в нашей предыдущей статье, опубликованной в этом журнале.

Политика безопасности P_k определяется формулой логики предикатов, представимой в виде конъюнкции определенных дизъюнктов Хорна: P_k C₁ ∧ C₂ ∧ …, здесь C_n – предложение политики вида:

∀х₁, …, x_m l₁(·) ∧ l₂(·) l₃(·) … Flow(u),

где u – связанная переменная или константа, обозначающая пользователя, Flow(u) – предикат, обозначающий легальность потока данных к u, l₁… l_n — условия (блокировки), выполнение которых требуется для того, чтобы Flow(u) принял значение TRUE. Предикаты l₁ … l_n могут быть параметрическими или непараметрическими.

Например, выражение политики: “Поток к произвольному пользователю x возможен, если а) открыта блокировка guest — для x задана роль guest – и открыта блокировка t_expire – истек заданный интервал времени или б) открыта блокировка manager — для x задана роль manager” – имеет формальный вид:

∀х. (t_expire ∧ guеst(x) ⇒ Flow(x)) ∧ ∧(manager(х) ⇒ Flow(x)).

Для описания политик в спецификации Paralocks.tla [6] вводятся следующие константы: UU — множество допустимых имен связанных переменных, U — множество актеров (конкретных пользователей системы), E₀ — множество имен непараметрических блокировок, E₁ — множество имен параметрических (с одним параметром) блокировок. Известные варианты использования Paralocks для кодирования политик элементов программной среды (переменных, параметров функций, исключений и т.д.), преемственных к наиболее распространенным механизмам управления доступом (мандатному, ролевому), позволяют ограничиться лишь непараметрическими и однопараметрическими блокировками, а также внести иные допущения, упрощающие описание соответствующих сущностей в спецификациях TLA+. Положим, что множество имен связанных переменных UU включает один элемент, также будем считать, что, если связанная переменная появляется в одной из блокировок некоторого предложения политики, то эта же переменная является аргументом и в литерале Flow(·) того же предложения, и если связанная переменная является аргументом Flow(·) некоторого предложения политики, то все параметрические блокировки того же предложения также будут принимать эту переменную в качестве аргумента.

Множество возможных предложений политик безопасности и множество самих политик определяются как:

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

Описанный ранее пример политики в спецификациях PLIF имеет вид ¹:

Здесь: x ∈ UU, t_expire ∈ E₀, {guest, reviewer, manager, organizer} ⊆ E₁, NONE — специальное значение, которое обозначает, что открытие блокировки не требуется (в TLA+ записи являются функциями, при этом частично определенные функции не поддерживаются).

Также с учетом заданных ограничений справедливы следующие предположения:

Пояснения к некоторым иным предположениям, заданным в Paralocks.tla и используемым в формальных доказательствах, приводятся несколько позже.

На множестве предложений политик безопасности задан оператор сравнения:

Оператор compareClause(c1, c2) возвращает значение TRUE – предложение c2 является как минимум таким же строгим, как и предложение c1 — если выполняются два условия: а) существует подстановка, приводящая предикат Flow(·) предложения c1 к виду, идентичному предикату Flow(·) предложения c2; б) после применения соответствующей подстановки к блокировкам предложения c1 множество блокировок предложения c1 будет представлять подмножество блокировок предложения c2. Логическая интерпретация заданного таким образом отношения частичного порядка приводится в [4].

Параметром предиката Flow(·) может выступать связанная переменная (элемент множества UU) или конкретный пользователь (элемент множества U), поэтому истинность первого условия определяется результатом вычисления функции:

В принятой нотации вторым элементом предложения политики является двумерный кортеж записей, определяющих необходимые наборы непараметрических и параметрических блокировок. Если открытие некоторой непараметрической блокировки не требуется, соответствующее поле записи принимает значение {NONE}, в противном случае – {}. Поэтому вхождение множества непараметрических блокировок предложения c1 во множество непараметрических блокировок предложения c2 фактически означает:

Для однопараметрических блокировок аналогично – значение {NONE} в поле соответствующей блокировки означает, что открытие блокировки не требуется. Если поле блокировки содержит не пустое множество элементов, отличных от {NONE}, значит, легитимность информационного потока к пользователю, заданному предикатом Flow(·), требует открытия некоторых экземпляров этой блокировки (определяются указанным множеством элементов). Функция matchLocks(·) применяет при необходимости соответствующую подстановку к выражениям однопараметрических блокировок предложения c1:

Для сравнения политик безопасности используется функция comparePol (·), ее определение тривиально:

Далее в пояснениях к выражениям TLAPS в некоторых случаях вместо compareClause(·) и comparePol (·) будем использовать оператор.

Наиболее важными правилами семантиками языка Paralocks являются правила вычисления наименьшей верхней (НВГ) и наибольшей нижней граней (ННГ) двух заданных политик безопасности. ННГ двух произвольных политик безопасности p1 и p2 является некоторая максимально строгая политика p_GLB, такая, что p_GLB ⊆ p1 и p_GLB ⊆ p2. Поскольку каждое предложение политики представляет собой отдельную возможность возникновения разрешенного информационного потока, очевидно, справедливо:

НВГ двух произвольных политик безопасности p1 и p2 является некоторая минимально строгая политика p_LUB, такая, что p1 ⊆ p_LUB и p2 ⊆ p_LUB. Для ее вычисления необходимо для всех возможных пар ⟨c1,c2⟩, таких, что c1 ∈ p1, c2 ∈ p2, и существует подстановка, приводящая предикат Flow(·) предложения c1 к виду, идентичному предикату Flow(·) предложения c2 или, наоборот, предикат Flow(·) предложения c2 — к виду, идентичному предикату Flow(·) предложения c1, сгенерировать новое предложение политики, применив соответствующую подстановку к блокировкам предложения c1 или c2 и объединив после этого полученные множества блокировок исходных предложений:

Здесь функция unionCl(c1, c2) вычисляет новое предложение политики p_LUB на основе предложений c1 и c2, если существует соответствующая подстановка, или возвращает пустое предложение ⟨⟩:

Локальная функция capMap объединяет непараметрические блокировки предложений c1 и c2 (поле, соответствующее непараметрической блокировке, принимает значение {NONE}, если блокировка не требуется, в противном случае — {}).

Для доказательства некоторых свойств с использованием TLAPS, как уже отмечалось, удобно использовать допущения – предположения (assumptions). Доказательство их справедливости иногда является нетривиальной задачей, а порой невозможной, поскольку TLAPS имеет ряд ограничений. Например, в системе отсутствует полноценная поддержка множеств, заданных с использованием кортежей. Проверка таких свойств с использованием механизма проигрывания моделей на неполных наборах данных не дает формальных гарантий. Для инвариантов типов проблема, как показывает исследование, может быть частично решена с использованием инструмента вывода типов Snowcat, который является частью платформы Apalache [10]. Еще одним предположением, используемым в доказательствах, является LUB_PS. Его обоснованность подтверждается проверкой с использованием Snowcat. Стоит отметить, однако, что использование указанного инструмента как правило требует специальной разметки спецификации:

Ряд иных тривиальных предположений, описанных в Paralocks.tla, в данной работе не разбирается.

3. ПРОВЕРКА СВОЙСТВ РЕШЕТКИ, ЗАДАННОЙ НА МНОЖЕСТВЕ ПОЛИТИК БЕЗОПАСНОСТИ

Процесс вывода формальных доказательств необходимых свойств алгебраических структур, описанных в спецификации Paralocks.tla, с использованием логической системы TLAPS является весьма трудоемким, поэтому на начальном этапе указанные свойства проверялись для ограниченного набора данных с использованием инструмента оценки выражений над константами среды TLA+Toolbox, а в некоторых случаях и с использованием инструмента проигрывания моделей TLC. Результаты предварительного этапа в данной работе не приводятся, однако их можно обнаружить в файлах проекта [6]. Представим общий вид доказательства того, что функция comparePol(·) является отношением частичного порядка на множестве политик PoliciesSet.

Рефлексивность

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

В первом случае очевидно:

∀c2 ∈ pol : (∃c1 ∈ pol : compareClause(c1,c2)),

доказательство следует из определения comparePol(·).

Во втором случае требуется для произвольного c1 ∈ pol доказать истинность compareClause(c1,c1) или с учетом определения compareClause(·):

Доказательство шага ⟨2⟩3 очевидно, оно следует из определения substMap3Equality(·) и истинности c1[1] = c1[1]. Шаг ⟨2⟩4 также не требует доказательства. Для доказательства шага ⟨2⟩3 интересен случай, когда c1[2][2][e] ≠ NONE.

В этом случае требуется доказательство истинности matchLocks(с1, с1, е) ⊆ с1[2][2][е]. Если с1[2][2][е] ∩ UU = {}, то доказательство следует из определения matchLocks (·) и истинности с1[2][2][e] ⊆⊆ с1[2][2][е]:

Для случая c1[2][2][e] ∩ UU ≠ {} доказательство легко может быть получено следующим образом:

Транзитивность

В виде теоремы в TLAPS свойство формулируется следующим образом:

Выбрав p1, p2, p3 из PoliciesSet и положив: comparePol(p1,p2) ∧ comparePol ( p2, p3), необходимо доказать: ∀c3 ∈ p3: (∃c1 ∈ p1 : compareClause(c1,c3)) [2]:

Очевидно, для любого c3 ∈ p3 можно найти такие c2 ∈ p2 и c1 ∈ p1, что справедливым будет: c2 ⊆ c3 ∧ c1 ⊆ c2. Тогда для доказательства теоремы достаточно выбрать соответствующие c1, c2, c3 и доказать справедливость c1 ⊆ c3 или с учетом определения substMap3Equality(·):

Доказательства шагов ⟨2⟩ 4 и ⟨2⟩ 5 следуют из истинности ⟨2⟩ 2, ⟨2⟩ 3 и определений: compareClause(·), substMap3Equality(·). Для доказательства шага ⟨2⟩ 6 интересен случай, когда c1[2][2][e] ≠ NONE:

В этом случае требуется доказательство истинности matchLocks(c1,c3,e) ⊆ c3[2][2][e]. Если c1[2][2][e] ∩ UU ≠ {}, доказательство может быть получено следующим образом:

Для случая c1[2][2][e] ∩ UU ={} доказательство выводится аналогично.

Антисимметричность

Свойство антисимметричности отношения частичного порядка на множестве политик безопасности PoliciesSet можно выразить следующим образом:

Общая схема доказательства не требует пояснений:

Доказательства шагов ⟨2⟩ 1 и ⟨2⟩ 2, очевидно, идентичны.

Рассмотрим далее структуру доказательства шага ⟨2⟩ 1. Предложение политики безопасности c, как уже отмечалось, состоит из трех компонент: предиката Flow(·) – c[1] (представлен параметром предиката), множества непараметрических блокировок и множества параметрических блокировок — c[2][1] и c[2][2] (имеют форму записей, в которых поля соответствуют наименованиям блокировок, значения — параметрам). Поэтому доказательство сводится к проверке эквивалентности соответствующих элементов:

На начальном этапе возьмем произвольное c2 из p2 и выберем такие c1 из p1 и c3 из p2, что c1 c2 и c3 c1. Докажем, что c3 = c2:

Поскольку выражение политики безопасности не может содержать двух различных предложений c1 и c2, таких, что c1 ⊆ c2 или c2 ⊆ c1, для доказательства шага ⟨3⟩ 6 достаточно доказать, что c3 ⊆ c2:

Истинность первых двух конъюнктов выражения compareClause(c3,c2) непосредственно следует из истинности шагов: ⟨3⟩ 3, ⟨3⟩ 4 (c1 ⊆ c2 ∧ c3 ⊆ c1), определения compareClause(·) и предположения о том, что для любого c, принадлежащего ClausesSet, справедливо: c[2][1] ∈ [E0 → {{NONE},{}}]:

Для доказательства истинности последнего условия выражения compareClause(c3,c2) необходимо рассмотреть три случая:

Доказательство шага ⟨5⟩ 2 тривиально. Доказательства шагов: ⟨5⟩ 3 и ⟨5⟩ 4 в полном объеме для краткости не приводятся. Отметим лишь, они основаны на том факте, что c1 ⊆ c2 ∧ c3 ⊆ c1, а также на предположениях: U_ASSM и UU_ASSM.

Опираясь на определения compareClause(·) и substMap3Equality(·), предположение о том, что множество допустимых связанных переменных состоит из одного элемента (UU_ASSM), а также на истинность шагов: ⟨3⟩ 3, ⟨3⟩ 4 и ⟨3⟩ 6 имеем: (c3[1] = x ∨ ∨c3[1] = c1[1]) ∧ (c1[1] = x ∨ c1[1] = c2[1]) ∧ c2[1] = = c3[1]. Отсюда следует истинность шага ⟨3⟩ 7 — c1[1] = c2[1]. Доказательство шага ⟨3⟩ 8 — c1[2][1] = = c2[2][1] — является также тривиальным.

Остается доказать истинность шага ⟨3⟩ 9 — c1[2][2] = c2[2][2]. Для этого достаточно выбрать произвольное значение e1 из E1 и доказать: c1[2][2][e1] =c2[2][2][e1]. Общая структура доказательства этого шага может быть представлена как:

Если c2[2][2][e1] = NONE, то из c1 ⊆ c2, определений compareClause(·) и matchLocks(·), предположений о представлении параметрических блокировок в предложениях политик безопасности, допустимых множествах связанных переменных и актеров следует:

Вывод доказательства для случая ⟨4⟩ 2 далее тривиален. Для шагов ⟨4⟩ 3 и ⟨4⟩ 4 c целью сохранить краткость изложения далее приводится лишь общая структура вывода, для которого ключевыми являются факты, определенные шагами: ⟨3⟩ 3, ⟨3⟩ 4 и ⟨3⟩ 6.

Полное доказательство транзитивности, заданного на множестве PoliciesSet отношения comparePol(·), можно найти в [6].

Решетка

Предположим, что заданная ранее функция LUB (·) действительно является функцией нахождения наименьшей верхней грани двух политик безопасности, и сформулируем в виде теоремы утверждение о том, что множество PoliciesSet с заданным на нем отношением частичного порядка comparePol(·) представляет собой алгебраическую решетку:

Отметим, даже на малых наборах данных (две параметрических блокировки, одна непараметрическая блокировка, один конкретный пользователь во множестве U, одна связанная переменная во множестве UU) проверить справедливость теоремы с использованием инструмента оценки выражений над константами среды TLA + Toolbox не удалось. На предварительном этапе пришлось воспользоваться инструментом проигрывания моделей TLC. В качестве переменных были выбраны: Policies2Set — множество всех возможных пар политик из множества PoliciesSet, curSet — текущая пара политик. LUB(p1, p2) – возвращает для пары политик p1 и p2 минимальную верхнюю грань, если она существует.

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

Доказательство шага ⟨1⟩ 4 строится на том факте, что любое предложение политики l является результатом применения некоторой подстановки к блокировкам предложения c1 или c2 с последующим объединением блокировок этих предложений — unionCl (c1,c2), где c1 ∈ p1 и c2 ∈ p2. Для доказательства шага ⟨1⟩ 5 в общем виде необходимо выбрать произвольную политику y ∈ PoliciesSet, произвольное предложение y1 ∈ y и доказать: ∃c1, c2, l1 : c1 ∈ p1 ∧ c2 ∈ p2 ∧ l1 ∈ l (c1 ⊆ y1 ∧ c2 ⊆ y1 => l1 ⊆ y1):

Далее необходимо сгенерировать некоторое предложение u = unionCl (c1, c2) и доказать: а) u принадлежит политике l = LUB (c1, c2) и б) u y ⊆ 1. Условие б) требует декомпозиции на три подусловия в соответствии с определением compareClause (·):

Здесь доказательство шага ⟨2⟩ 25 является наиболее трудоемким и требует рассмотрения трех случаев. В целом логический вывод доказательств для каждого из них осуществляется в таком же стиле, что и выводы доказательств для аналогичных этапов ранее рассмотренных утверждений – последовательная проверка выражений функции compareClause(·), отвечающих за сравнение параметрических блокировок предложений политики безопасности, с опорой на определенный набор обоснованных предположений.

4. ЗАКЛЮЧЕНИЕ

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

Представленное исследование обладает самостоятельной ценностью, поскольку дает вариант описания политик Paralocks, имеющих внедрение в Java (проект Paragon [13], [11]), в формальном языке TLA+, который часто применяется для моделирования программ и проверки их свойств. Таким образом, в работе делается шаг в сторону создания применимой на практике платформы КИП, основанной на методах формальной верификации и проигрывания моделей.

Сама идея проверки безопасности информационных потоков на основе методов формальной верификации ранее выдвигалась и получила определенное признание [14]. Однако в указанной работе проводились только теоретические исследования, не привязанные к конкретному языку программирования, алфавит политик безопасности в ней представлен простой двухуровневой решеткой ⟨{Hi,Low}, ⊆⟩.

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

Практическое значение может иметь предложенный вариант использования формальной логической системы TLAPS. Как уже отмечалось, многие объемные доказательства, публикуемые в современных статьях, содержат некорректные утверждения. Человеческий фактор является причиной возникновения простейших ошибок. Например, часто на основе установленного (заданного) факта вида: “∀x ∈ X выполняется P(x)” делается шаг: “возьмем x ∈ X, для которого выполняется P(x)”. Шаг является некорректным, так как требует проверки дополнительного условия “X не является пустым”. Другим ошибочным примером является использование для доказательства истинности некоторого утверждения фактов вида: x1 = if e1 then x2 else x3 и x1 = x2. Недостающим условием в данном случае является: x2 ≠ x3, его проверка может оказаться нетривиальной.

Использование таких средств, как TLAPS, безусловно влечет дополнительные трудозатраты, вызванные необходимостью трансляции доказательств в формулы TLA+, но в то же время предоставляет дополнительные гарантии корректности получаемых результатов.

5. БЛАГОДАРНОСТИ

Автор выражает признательность Джуру Куковецу (Институт разработки информационных систем, Вена, https://informatics.tuwien.ac.at/orgs/e194), одному из разработчиков инструмента Apalache [10], предназначенного для проверки спецификаций TLA+ на основе символьного выполнения, за важные рекомендации по оптимизации отдельных функций и операторов, образующих TLA+ семантику используемой версии языка Paralocks. Несмотря на то, что на данном этапе полностью адаптировать спецификации PLIF для применения Apalache не удалось, дальнейшая работа в этом направлении, по мнению автора, имеет перспективу и будет продолжена.

¹ Для интерпретации трасс, приводящих к ошибкам, PLIF используется упрощенная нотация, в которой пример выглядит как:

² Доказательство опирается на определения функций: ComparePol(·), CompareClause(·), substMap3Equality(·) и MatchLocks(·).

Sobre autores

A. Timakov

Autor responsável pela correspondência
Email: timakov@mirea.ru
ORCID ID: 0000-0003-4306-789X
Rússia, Pr. Vernadskogo 78, Moscow, 119454

Bibliografia

Arquivos suplementares

Arquivos suplementares

Ação

1. JATS XML

Baixar

2. Fig.1

Baixar (84KB)

Metadados

3. Fig.2

Baixar (67KB)

Metadados

4. Fig.3

Baixar (64KB)

Metadados

5. Fig.4

Baixar (60KB)

Metadados

6. Fig.5

Baixar (22KB)

Metadados

7. Fig.6

Baixar (20KB)

Metadados

8. Fig.7

Baixar (32KB)

Metadados

9. Fig.8

Baixar (25KB)

Metadados

10. Fig.9

Baixar (13KB)

Metadados

11. Fig.10

Baixar (23KB)

Metadados

12. Fig.11

Baixar (99KB)

Metadados

13. Fig.12

Baixar (76KB)

Metadados

14. Fig.13

Baixar (40KB)

Metadados

15. Fig.14

Baixar (14KB)

Metadados

16. Fig.15

Baixar (57KB)

Metadados

17. Fig.16

Baixar (57KB)

Metadados

18. Fig.17

Baixar (3KB)

Metadados

19. Fig.18

Baixar (37KB)

Metadados

20. Fig.19

Baixar (57KB)

Metadados

21. Fig.20

Baixar (29KB)

Metadados

22. Fig.21

Baixar (57KB)

Metadados

23. Fig.22

Baixar (87KB)

Metadados

24. Fig.23

Baixar (18KB)

Metadados

25. Fig.24

Baixar (31KB)

Metadados

26. Fig.25

Baixar (99KB)

Metadados

27. Fig.26

Baixar (25KB)

Metadados

28. Fig.27

Baixar (60KB)

Metadados

29. Fig.28

Baixar (42KB)

Metadados

30. Fig.29

Baixar (29KB)

Metadados

31. Fig.30

Baixar (7KB)

Metadados

32. Fig.31

Baixar (23KB)

Metadados

33. Fig.32

Baixar (70KB)

Metadados

34. Fig.33

Baixar (31KB)

Metadados

35. Fig.34

Baixar (45KB)

Metadados

36. Fig.35

Baixar (48KB)

Metadados

37. Fig.36

Baixar (39KB)

Metadados

38. Fig.37

Baixar (35KB)

Metadados

39. Fig.38

Baixar (84KB)

Metadados

40. Fig.39

Baixar (53KB)

Metadados

41. Fig.40

Baixar (45KB)

Metadados

42. Fig.41

Baixar (47KB)

Metadados

43. Fig.42

Baixar (75KB)

Metadados

44. Fig.43

Baixar (101KB)

Metadados

45. Fig.44

Baixar (100KB)

Metadados

46. Fig.45

Baixar (29KB)

Metadados