И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin (1161239), страница 12
Текст из файла (страница 12)
*/if:: (data.key == pkA) && (data.d1 == nonceA) &&(data.s == partnerA) && (data.r == alice) &&(data.nummsg == 2)->pnonce = data.d2;:: else -> goto stopA;fi;/* отвечает сообщением №3 и успешно завершается*/d_step {data.s = alice;data.r = partnerA;data.nummsg = 3;data.key = pkey;data.d1 = pnonce;data.d2 = 0;}intercepted ! msg(data);statusA = ok;stopA:printf("MSC: Process A finished \n");} /* proctype Alice() *//* Честный партнер по обмену */active proctype Bob() {mtype pkey, pnonce, receiver, partner;mesCrypt data;statusB = err;/* ожидает сообщения msg1, идентифицирует партнера */fakedB ? msg(data);/* проверяет сообщение на правильность построения,если что-то не соответствует ожиданию, останавливается */end_errB1:if:: (data.r == bob) && (data.key == pkB) && (data.s == data.d1) &&(data.nummsg == 1)->partnerB = data.s;pnonce = data.d2;:: else -> goto stopB;fi;/* устанавливает публичный ключ партнера */if:: (partnerB == alice) -> pkey = pkA;:: (partnerB == intruder) -> pkey = pkI;:: else -> goto stopB;fi;/* отвечает сообщением № 2 */d_step {data.s = bob;data.r = partnerB;data.nummsg = 2;52data.key = pkey;data.d1 = pnonce;data.d2 = nonceB;}intercepted ! msg(data);/* ожидает № 3, проверяет сообщение на корректность,и в случае успеха завершается в состоянии ok */fakedB ? msg(data);end_errB2:if:: (data.r == bob) && (data.s == partnerB) && (data.key == pkB) &&(data.d1 == nonceB) && (data.nummsg == 3)->statusB = ok;:: else -> goto stopB;fi;stopB:printf("MSC: Process B finished \n");}/* Злоумышленник не следует детерминированному алгоритму*/active proctype Intruder() {mesCrypt data, fake;knowNA = false;knowNB = false;end: do:: intercepted ? msg(data) ->if:: (data.key == pkI) ->if:: (data.d1 == nonceA || data.d2 == nonceA) -> knowNA = true;:: (data.d1 == nonceB || data.d2 == nonceB) -> knowNB = true;fi;:: else -> skip;fi;/* построение испорченного сообщения */if:: fake.s = alice ->fake.r = bob; fake.key = pkB;:: fake.s = bob;fake.r = alice; fake.key = pkA;:: fake.s = intruder;if:: fake.r = bob; fake.key = pkB;:: fake.r = alice; fake.key = pkA;fi;fi;/* злоумышленник не знает правила построения сообшения */if:: fake.d1 = alice;:: fake.d1 = bob;:: fake.d1 = intruder;:: fake.d1 = nonceI;:: (knowNA) -> fake.d1 = nonceA;:: (knowNB) -> fake.d1 = nonceB;fi;53if:: fake.d2 = alice;:: fake.d2 = bob;:: fake.d2 = intruder;:: fake.d1 = nonceI;:: (knowNA) -> fake.d2 = nonceA;:: (knowNB) -> fake.d2 = nonceB;fi;/* вставляет в сообщение неизвестную зашифрованную частьиз полученного сообщения */if:: (data.key != pkI) ->fake.key = data.key;fake.d1 = data.d1;fake.d2 = data.d2;:: else -> skip;fi;/* выбираем номер сообщения */if:: fake.nummsg = 1;:: fake.nummsg = 2;:: fake.nummsg = 3;fi;}od;if:: (data.r ==fakedA !:: (data.r ==fakedB !:: (fake.r ==fakedA !:: (fake.r ==fakedB !fi;alice) ->msg(data);bob) ->msg(data);alice)msg(fake);bob)msg(fake);/* повторяем полученное сообщение*//* повторяем полученное сообщение*//* отправляем испорченное сообщение *//* отправляем испорченное сообщение */Поиск криптографической атакиВ описанном алгоритме атакой можно считать ситуацию, когда сторона В будет считатьсвоим партнером сторону А, сторона A будет доверять своему партнеру, а злоумышленникбудет знать обе части их секрета.
Сформулируем эту ситуацию в виде LTL формулы: "несуществует такого пути в системе, что когда-нибудь в будущем сторона В, успешнозавершив работу, будет полагать, что ее партнер А, и подслушивающий при этом знаетnonceA и nonceB"<> ( agentB_finished && bobtrustsA && intrknowNA && intrknowNB )где предикаты заданы следующим образом (переменные statusB, partnerB, knowNA,knowNB определены в теле программы)#define#define#define#defineagentB_finished (statusB == ok)bobtrustsA(partnerB == alice)intrknowNA(knowNA == true)intrknowNB(knowNB == true)Поставив флаг No Executions для заданной формулы, запустим верификатор Spin.
Spinобнаружил атаку, описанную Лоуве в 1995 году.541. Alice, считая Intruder честной стороной, посылает ему сообщение № 1 со своимидентификатором и своей частью секретного ключа, зашифровав все публичнымключом Intruder [16 -> 17]. Intruder уже известен nonceA.2. Intruder посылает сообщение № 1 Bob, поставив в открытую часть сообщения вкачестве отправителя Alice, а далее повторив ее письмо себе, зашифровав секретнуючасть публичным ключом Bob [39-40].3. Bob отвечает Intruder сообщением№ 2, полагая, что тот является Alice.Вписьмесодержитсячасть,непонятная Intruder, поскольку оназашифрованапубличнымключомAlice [54-55]. В зашифрованной частиписьма идет nonceB – часть секретаBob,ноонанедоступназлоумышленнику.4.
Злоумышленникотправляетсообщение № 2 Alice [73-74]. Вкачестве основы он берет сообщениеBob,зашифрованнуючастьонвставляет целиком, а в открытой частименяет отправителя на себя.5. Alice,доверяяIntruder,расшифровывает сообщение № 2,извлекает nonceB, отвечает Intruderсообщением№3, содержащимnonceB, при чем секретная частьзашифрованапубличнымключомIntruder [82-83].6. Intruder расшифровывает сообщение№ 3, узнает nonceB, посылает сообщение № 3 Bob. Полученное сообщение проходитвсе проверки Bob, и он успешно завершает работу [105-106].3.4Задача об обедающих философахОписание алгоритмаЗнаменитая задача об обедающих философах, предложенная Эдсгером Дейкстрой, являетсяобразным описанием – метафорой, позволяющей ясно представить проблемы, возникающиепри совместном использовании ресурсов несколькими параллельными процессами.За круглым столом сидят несколько философов, каждый из которых проводит время вразмышлениях, изредка прерываясь на еду, когда он проголодается.
На столе стоит блюдо соспагетти и вилки, по одной между каждыми двумя философами. Для того чтобы поесть,каждый философ должен использовать две вилки, которые лежат непосредственно слева исправа от него. Проголодавшись, он по очереди берет вилки, если они не заняты, естспагетти, после чего возвращает вилки на место и продолжает думать до тех пор, пока сноване проголодается, затем опять ест и т.д.
Если правая либо левая вилка занята соседом,философ просто ждет ее освобождения.55Сформулированная таким образом ситуация кажется совершенно безобидной, поведениекаждого процесса очевидно, и трудно предположить, что в этой просто сформулированнойситуации могут возникнуть проблемы. В то же время формальное представление ситуации ввиде параллельных процессов, когда философы представляют процессы, а вилкипредставляют общие ресурсы, демонстрирует возможность возникновения блокировкипроцессов, конкурирующих за разделяемые ресурсы.
Такая блокировка возникает оченьредко, но она приводит к остановке всех процессов. На языке метафоры это означает, чтоможет сложиться условие, при которой все философы, упрямо следующие своим правиламповедения (фактически, просто выполняющие свой алгоритм поведения), умрут голоднойсмертью даже при наличии полного блюда спагетти.Построим формальное описание ситуации.
Опишем возможные состояния философа:S0. Философ размышляет. В этом состоянии он может проголодаться, что представляетсяспонтанным переходом в состояние S1.S1. В этом состоянии философ хочет есть, поэтому ему требуются вилки. Философ тянется завилкой, лежащей слева от него. Если эта вилка отсутствует, то он в состоянии S1 ждет ееосвобождения. Если левая вилка свободна, то он ее берет и переходит в состояние S2.S2. В этом состоянии философ ожидает правую вилку.
Если правая вилка отсутствует, то онбудет находиться в этом состоянии до ее освобождения. Если правая вилка свободна, тоон ее берет и переходит в состояние S3 – имея обе вилки, он в этом состоянии естспагетти.S3. Философ ест. После того, как он поел, он кладет на стол левую вилку, переходя вследующее состояние S4.S4. В этом состоянии философ кладет на стол правую вилку и возвращается к размышлениям(в состояние S0).Возможные состояния каждой вилки:F0.
Вилка свободна. Она лежит на столе и готова к тому, что ее возьмет один из философов(слева или справа). Если ее берет левый философ, она переходит в состояние F1, если ееберет правый философ, она переходит в состояние F2.F1. Вилка находится у философа слева и ожидает возвращения на стол (состояние F0).F2. Вилка находится у философа справа и ожидает возвращения на стол (состояние F0).Возможна ли ситуация общего голодания, т.е. когда все философы не смогут поесть из-заотсутствия у них необходимых вилок?Мы обнаружим ситуацию общего голодания при помощи пакета верификации параллельныхпроцессов SPIN.Описание модели на языке PromelaРешаем задачу для N философов. Введем в модель 2N процессов: N процессов потребуетсядля описания поведения философов и N процессов – для описания поведения вилок.Состояние философа фиксируем в переменной cur_state. Взятию вилки философом и еевозвращению (освобождению) сопоставим передачу сообщения по рандеву-каналу отфилософа к вилке.
Всего вводится 2N каналов.chan l_fork[N] = [0] of {bit}; /* Для левой к философу вилки */chan r_fork[N] = [0] of {bit}; /* Для правой к философу вилки */Каждому философу необходимо два канала – один для организации обмена с левой вилкой,другой – для организации обмена с правой вилкой. Использование рандеву-каналов56гарантирует синхронизацию взаимодействия между философом и вилкой: философ получитвилку только тогда, когда вилка будет свободна; лежащая на столе вилка поступит враспоряжение философа только тогда, когда философ ее запросит.Для передачи запроса о доступе к вилке и об ее освобождении будет достаточно сообщенийодного типа:#define msgtype 1/* тип сообщения */которые фактически будут играть роль сигнала для вилки и философа для изменениясостояния.proctype phil (chan left, right; byte mn){byte cur_state = 0;printf("MSC: phil # %d \n", mn);do::::(cur_state == 1)left ! msgtypecur_state = 2;->->(cur_state == 2) ->right ! msgtype;cur_state = 3;::(cur_state == 3) ->cur_state = 4;:: (cur_state == 4) ->right ! msgtype ->cur_state = 5;:: (cur_state == 5) ->left ! msgtype ->cur_state = 0;::(cur_state == 0) ->cur_state = 1;}/* Философ запросил левую вилку *//* Философ запросил правую вилку *//* Философ ест *//* Философ наелся *//* Философ вернул правую вилку *//* Философ вернул левую вилку *//* Философ размышляет *//* Философ решил поесть */odДля хранения состояния процесса-вилки используется переменная cur_state_fork.Взаимодействие с философами осуществляется по тем же рандеву-каналам – по одномуканалу на каждого философа (один канал для левого философа, один для правого).
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
