- Изменения мощности и потока информации на ЭЭГ в состоянии покоя с помощью процесса рабочей памяти(arXiv)
Автор:Ги-Хван Шин, Ён-Сок Квон, Хон-Гю Квак
Аннотация: во многих исследованиях анализируется рабочая память (РП) по данным электроэнцефалограммы (ЭЭГ). Однако мало что известно об изменениях нейродинамики головного мозга в состоянии покоя (RS) в зависимости от процесса WM. Здесь мы идентифицировали частотно-специфические модели мощности и потока информации среди трех RS ЭЭГ до и после кодирования WM и извлечения WM. Наши результаты продемонстрировали разницу в мощности и информационном потоке РС ЭЭГ в дельта (1–3,5 Гц), альфа (8–13,5 Гц) и бета (14–29,5 Гц) диапазонах. В частности, наблюдалось заметное увеличение альфа-диапазона после извлечения WM. Кроме того, мы рассчитали связь между значимыми характеристиками РС ЭЭГ и производительностью WM, и, что интересно, корреляции были обнаружены только в альфа-диапазоне. Эти результаты свидетельствуют о том, что РС ЭЭГ в соответствии с процессом WM оказывает значительное влияние на вариабельность и производительность WM механизмов мозга в отношении когнитивных функций.
2.CommCSL: Доказательство безопасности информационных потоков для параллельных программ с использованием абстрактной коммутативности(arXiv)
Автор:Марко Эйлерс, Тибо Дардинье, Питер Мюллер
Вывод:безопасность информационного потока гарантирует, что секретные данные, которыми манипулирует программа, не влияют на ее наблюдаемые выходные данные. Доказательство безопасности информационных потоков особенно сложно для параллельных программ, где операции с секретными данными могут повлиять на время выполнения потока и, таким образом, на чередование между различными потоками. Такие внутренние каналы синхронизации могут повлиять на наблюдаемый результат программы, даже если злоумышленник не следит за временем выполнения. Существующие методы проверки безопасности информационных потоков в параллельных программах пытаются доказать, что секретные данные не влияют на относительную синхронизацию потоков. Однако эти методы часто ограничивают (например, потому что они запрещают ветвление на секретных данных) и делают серьезные предположения о платформе выполнения (игнорируя кэширование, инструкции процессора с зависимой от данных средой выполнения и другие общие функции, влияющие на время выполнения). В этой статье мы представляем новый метод проверки безопасного потока информации в параллельных программах, который снимает эти ограничения и не делает никаких предположений о временных характеристиках. Ключевая идея состоит в том, чтобы доказать, что все операции изменения, выполняемые с общими данными, коммутируют, так что различные чередования потоков не влияют на его конечное значение. Важно отметить, что коммутативность требуется только для абстракции общих данных, содержащих информацию, которая будет передана в открытый доступ. Абстрактная коммутативность удовлетворяется гораздо большим количеством операций, чем стандартная коммутативность, что делает нашу технику широко применимой. Мы формализуем нашу технику в CommCSL, реляционной параллельной логике разделения с поддержкой рассуждений, основанных на коммутативности, и докажем ее правильность в Isabelle/HOL. Мы внедрили CommCSL в HyperViper, автоматизированный верификатор, основанный на инфраструктуре верификации Viper, и продемонстрировали его способность проверять сложный пример.
